structured a proof

[helm.git] / helm / matita / library / nat / factorization.ma

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index 6a309430302ee18b576e2def76303d3333a6fdfd..37b5ea1ddb8e5d82d19ff44acc362d07f0fbb8ce 100644 (file)
--- 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