From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 26 Jul 2006 09:24:55 +0000 (+0000)
Subject: added tinycals to the proof we frequently use for examples and screenshots
X-Git-Tag: 0.4.95@7852~1147
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c698212feffe7bb3119b62533a58132401668be;p=helm.git

added tinycals to the proof we frequently use for examples and screenshots
---

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.