added a function to reorder the metasenv.

[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 30174d7707fd7ced16705d2f1832fce95d108b26..a3a71522804d7eee69c2f5461d3fd7fe79d73fbf 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -189,9 +189,6 @@ cut n1 = r*(exp (nth_prime n) q).
 rewrite > H.
 simplify.rewrite < assoc_times.
 rewrite < Hcut.reflexivity.
-rewrite > sym_times.
-apply plog_aux_to_exp n1 n1.
-apply lt_O_nth_prime_n.assumption.
 cut O < r \lor O = r.
 elim Hcut1.assumption.absurd n1 = O.
 rewrite > Hcut.rewrite < H4.reflexivity.
@@ -227,6 +224,9 @@ assumption.
 apply le_to_or_lt_eq r (S O).
 apply not_lt_to_le.assumption.
 apply decidable_lt (S O) r.
+rewrite > sym_times.
+apply plog_aux_to_exp n1 n1.
+apply lt_O_nth_prime_n.assumption.
 qed.
 
 theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
@@ -274,35 +274,20 @@ rewrite > Hcut3 in \vdash (? (? ? %)).
 change with divides (nth_prime p) r \to False.
 intro.
 apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?.
-apply divides_to_mod_O.
-apply lt_O_nth_prime_n.
-assumption.
 apply lt_SO_nth_prime_n.
-simplify.apply le_S_S.apply le_O_n.
-apply le_n.
-assumption.rewrite > times_n_SO in \vdash (? ? ? %).
+simplify.apply le_S_S.apply le_O_n.apply le_n.
+assumption.
+apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
+rewrite > times_n_SO in \vdash (? ? ? %).
 rewrite < sym_times.
 rewrite > exp_n_O (nth_prime p).
 rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
 assumption.
-apply le_to_or_lt_eq.apply le_O_n.
-(* O < r *)
-cut O < r \lor O = r.
-elim Hcut1.assumption.
-apply False_ind.
-apply not_eq_O_S (S m1).
-rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
-apply le_to_or_lt_eq.apply le_O_n.
-(* prova del cut *)
-apply plog_aux_to_exp (S(S m1)).
-apply lt_O_nth_prime_n.
-assumption.
-(* fine prova cut *)
-assumption.
-(* e adesso l'ultimo goal *)
+apply le_to_or_lt_eq.apply le_O_n.assumption.
+(* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
 cut (S O) < r \lor \lnot (S O) < r.
 elim Hcut2.
-right.
+right. 
 apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r.
 simplify.apply le_S_S. apply le_O_n.
 apply le_n.
@@ -321,6 +306,19 @@ rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply le_to_or_lt_eq r (S O).
 apply not_lt_to_le.assumption.
 apply decidable_lt (S O) r.
+(* O < r *)
+cut O < r \lor O = r.
+elim Hcut1.assumption. 
+apply False_ind.
+apply not_eq_O_S (S m1).
+rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
+apply le_to_or_lt_eq.apply le_O_n.
+(* prova del cut *)
+goal 20.
+apply plog_aux_to_exp (S(S m1)).
+apply lt_O_nth_prime_n.
+assumption.
+(* fine prova cut *)
 qed.
 
 let rec max_p f \def
@@ -403,7 +401,8 @@ cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H4.
 apply H i (S j) ?.
-assumption.apply trans_lt ? j.assumption.simplify.apply le_n.
+apply trans_lt ? j.assumption.simplify.apply le_n.
+assumption.
 apply divides_times_to_divides.
 apply prime_nth_prime.assumption.
 qed.
@@ -472,23 +471,23 @@ rewrite > plus_n_O.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
 apply False_ind.
 apply not_divides_defactorize_aux n1 i (S i) ?.
+simplify. apply le_n.
 simplify in H5.
 rewrite > plus_n_O (defactorize_aux n1 (S i)).
 rewrite > H5.
 rewrite > assoc_times.
 apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))).
 reflexivity.
-simplify. apply le_n.
 intros.
 apply False_ind.
 apply not_divides_defactorize_aux n3 i (S i) ?.
+simplify. apply le_n.
 simplify in H4.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).
 rewrite < H4.
 rewrite > assoc_times.
 apply witness ? ? ((exp (nth_prime i) n4)*(defactorize_aux n1 (S i))).
 reflexivity.
-simplify. apply le_n.
 intros.
 cut nf_cons n4 n1 = nf_cons m n3.
 cut n4=m.