From 82ec52f9e431b17659033cbfdcaa56c44d9e285d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 30 Jan 2006 14:49:16 +0000 Subject: [PATCH] structured a proof --- helm/matita/library/nat/factorization.ma | 50 +++++++++++++----------- 1 file changed, 28 insertions(+), 22 deletions(-) diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index 6a3094303..37b5ea1dd 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -24,28 +24,34 @@ definition max_prime_factor \def \lambda n:nat. (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)). (* max_prime_factor is indeed a factor *) -theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to -nth_prime (max_prime_factor n) \divides n. -intros.apply divides_b_true_to_divides. -apply lt_O_nth_prime_n. -apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n). -cut (\exists i. nth_prime i = smallest_factor n). -elim Hcut. -apply (ex_intro nat ? a). -split. -apply (trans_le a (nth_prime a)). -apply le_n_fn. -exact lt_nth_prime_n_nth_prime_Sn. -rewrite > H1. apply le_smallest_factor_n. -rewrite > H1. -change with (divides_b (smallest_factor n) n = true). -apply divides_to_divides_b_true. -apply (trans_lt ? (S O)).unfold lt. apply le_n. -apply lt_SO_smallest_factor.assumption. -apply divides_smallest_factor_n. -apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption. -apply prime_to_nth_prime. -apply prime_smallest_factor_n.assumption. +theorem divides_max_prime_factor_n: + \forall n:nat. (S O) < n + \to nth_prime (max_prime_factor n) \divides n. +intros; apply divides_b_true_to_divides; +[ apply lt_O_nth_prime_n; +| apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n); + cut (\exists i. nth_prime i = smallest_factor n); + [ elim Hcut. + apply (ex_intro nat ? a); + split; + [ apply (trans_le a (nth_prime a)); + [ apply le_n_fn; + exact lt_nth_prime_n_nth_prime_Sn; + | rewrite > H1; + apply le_smallest_factor_n; ] + | rewrite > H1; + change with (divides_b (smallest_factor n) n = true); + apply divides_to_divides_b_true; + [ apply (trans_lt ? (S O)); + [ unfold lt; apply le_n; + | apply lt_SO_smallest_factor; assumption; ] + | apply divides_smallest_factor_n; + apply (trans_lt ? (S O)); + [ unfold lt; apply le_n; + | assumption; ] ] ] + | apply prime_to_nth_prime; + apply prime_smallest_factor_n; + assumption; ] ] qed. theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to -- 2.39.2