X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ffactorization.ma;h=6a309430302ee18b576e2def76303d3333a6fdfd;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=b64e3733b5fbe0e5b5de21e15e9ad957e49982f3;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index b64e3733b..6a3094303 100644
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -40,10 +40,10 @@ 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)).simplify. apply le_n.
+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)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 apply prime_to_nth_prime.
 apply prime_smallest_factor_n.assumption.
 qed.
@@ -167,7 +167,7 @@ match f with
 
 theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 O < defactorize_aux f i.
-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt. 
 rewrite > times_n_SO.
 apply le_times.
 change with (O < nth_prime i).
@@ -175,7 +175,7 @@ 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.
+simplify.unfold lt.
 rewrite > times_n_SO.
 apply le_times.
 change with (O < exp (nth_prime i) n).
@@ -187,7 +187,7 @@ qed.
 
 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 S O < defactorize_aux f i.
-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt.
 rewrite > times_n_SO.
 apply le_times.
 change with (S O < nth_prime i).
@@ -195,7 +195,7 @@ apply lt_SO_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.
-simplify.
+simplify.unfold lt.
 rewrite > times_n_SO.
 rewrite > sym_times.
 apply le_times.
@@ -233,7 +233,7 @@ rewrite < Hcut.reflexivity.
 cut (O < r \lor O = r).
 elim Hcut1.assumption.absurd (n1 = O).
 rewrite > Hcut.rewrite < H4.reflexivity.
-simplify. intro.apply (not_le_Sn_O O).
+unfold Not. intro.apply (not_le_Sn_O O).
 rewrite < H5 in \vdash (? ? %).assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 cut ((S O) < r \lor (S O) \nlt r).
@@ -251,11 +251,11 @@ cut (r=(S O)).
 apply (nat_case n).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut2.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
 cut (r \lt (S O) \or r=(S O)).
 elim Hcut2.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
-simplify.intro.
+unfold Not.intro.
 cut (O=n1).
 apply (not_le_Sn_O O).
 rewrite > Hcut3 in \vdash (? ? %).
@@ -309,14 +309,14 @@ cut (O < q \lor O = q).
 elim Hcut2.assumption.
 absurd (nth_prime p \divides S (S m1)).
 apply (divides_max_prime_factor_n (S (S m1))).
-simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
 cut ((S(S m1)) = r).
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with (nth_prime p \divides r \to False).
 intro.
 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
 apply lt_SO_nth_prime_n.
-simplify.apply le_S_S.apply le_O_n.apply le_n.
+unfold lt.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 (? ? ? %).
@@ -330,18 +330,18 @@ cut ((S O) < r \lor S O \nlt r).
 elim Hcut2.
 right. 
 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
-simplify.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S. apply le_O_n.
 apply le_n.
 assumption.assumption.
 cut (r=(S O)).
 apply (nat_case p).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut3.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
 cut (r \lt (S O) \or r=(S O)).
 elim Hcut3.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
-simplify.intro.
+unfold Not.intro.
 apply (not_le_Sn_O O).
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply (le_to_or_lt_eq r (S O)).
@@ -406,11 +406,11 @@ theorem divides_exp_to_eq:
 \forall p,q,m:nat. prime p \to prime q \to
 p \divides q \sup m \to p = q.
 intros.
-simplify in H1.
+unfold prime in H1.
 elim H1.apply H4.
 apply (divides_exp_to_divides p q m).
 assumption.assumption.
-simplify in H.elim H.assumption.
+unfold prime in H.elim H.assumption.
 qed.
 
 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
@@ -442,7 +442,7 @@ cut (i = j).
 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply (injective_nth_prime ? ? H4).
 apply (H i (S j)).
-apply (trans_lt ? j).assumption.simplify.apply le_n.
+apply (trans_lt ? j).assumption.unfold lt.apply le_n.
 assumption.
 apply divides_times_to_divides.
 apply prime_nth_prime.assumption.
@@ -473,10 +473,10 @@ qed.
 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 intros.
-simplify.rewrite < plus_n_O.
+simplify.unfold Not.rewrite < plus_n_O.
 intro.
 apply (not_divides_defactorize_aux f i (S i) ?).
-simplify.apply le_n.
+unfold lt.apply le_n.
 rewrite > H.
 rewrite > assoc_times.
 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).