X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ffactorization.ma;h=e61658786ce7095a3007a0590d51de9aeb66d80a;hb=216686b3739474d279c87892892af82c5ea5aec3;hp=715a9795f1dc8d8115049931277a7022a166ed60;hpb=04e27500136c94e4f2ac072a5e4d330b75da35f0;p=helm.git

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 715a9795f..e61658786 100644
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -169,24 +169,23 @@ match f with
 | nfa_one \Rightarrow (S O)
 | (nfa_proper g) \Rightarrow defactorize_aux g O]. 
 
-theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
-O < defactorize_aux f i.
-intro.elim f.simplify.unfold lt. 
-rewrite > times_n_SO.
-apply le_times.
-change with (O < nth_prime i).
-apply lt_O_nth_prime_n.
-change with (O < exp (nth_prime i) n).
-apply lt_O_exp.
-apply lt_O_nth_prime_n.
-simplify.unfold lt.
-rewrite > times_n_SO.
-apply le_times.
-change with (O < exp (nth_prime i) n).
-apply lt_O_exp.
-apply lt_O_nth_prime_n.
-change with (O < defactorize_aux n1 (S i)).
-apply H.
+theorem lt_O_defactorize_aux:
+ \forall f:nat_fact.
+ \forall i:nat.
+ O < defactorize_aux f i.
+intro; elim f;
+[1,2:
+  simplify; unfold lt;
+  rewrite > times_n_SO;
+  apply le_times;
+  [ change with (O < nth_prime i);
+    apply lt_O_nth_prime_n;
+  |2,3:
+    change with (O < exp (nth_prime i) n);
+    apply lt_O_exp;
+    apply lt_O_nth_prime_n;
+  | change with (O < defactorize_aux n1 (S i));
+    apply H; ] ]
 qed.
 
 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.