X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=65f61b581691cdabbdaeeb34fc7d10ac21927a93;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=d42a57e8e8db6c1661d480d829bcf1d6289c96de;hpb=cca04138889cd0dbafb669a5c3fd8abe424d699e;p=helm.git

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index d42a57e8e..65f61b581 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -136,7 +136,7 @@ intros.change with
 \land 
 gcd_aux (S m1) m (S m1) \divides (S m1)).
 apply divides_gcd_aux_mn.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 assumption.apply le_n.
 simplify.intro.
 apply (nat_case1 m).
@@ -152,8 +152,8 @@ cut (gcd_aux (S m1) n (S m1) \divides n
 gcd_aux (S m1) n (S m1) \divides S m1).
 elim Hcut.split.assumption.assumption.
 apply divides_gcd_aux_mn.
-simplify.apply le_S_S.apply le_O_n.
-apply not_lt_to_le.simplify.intro.apply H.
+unfold lt.apply le_S_S.apply le_O_n.
+apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
 rewrite > H1.apply (trans_le ? (S n)).
 apply le_n_Sn.assumption.apply le_n.
 qed.
@@ -221,13 +221,13 @@ apply (nat_case1 n).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) m (S m1)).
 apply divides_gcd_aux.
-simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
+unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
 rewrite < H2.assumption.
 apply (nat_case1 m).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) n (S m1)).
 apply divides_gcd_aux.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 rewrite < H2.assumption.
 qed.
@@ -343,7 +343,7 @@ change with
 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 apply eq_minus_gcd_aux.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 assumption.apply le_n.
 apply (nat_case1 m).
 simplify.intros.
@@ -370,7 +370,7 @@ apply (ex_intro ? ? a1).
 apply (ex_intro ? ? a).
 left.assumption.
 apply eq_minus_gcd_aux.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply lt_to_le.apply not_le_to_lt.assumption.
 apply le_n.
 qed.
@@ -397,7 +397,7 @@ intros.
 generalize in match (gcd_O_to_eq_O m n H1).
 intros.elim H2.
 rewrite < H4 in \vdash (? ? %).assumption.
-intros.simplify.apply le_S_S.apply le_O_n.
+intros.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
@@ -435,7 +435,7 @@ intro.
 apply divides_to_le.
 apply lt_O_gcd.
 rewrite > (times_n_O O).
-apply lt_times.simplify.apply le_S_S.apply le_O_n.assumption.
+apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
 apply divides_d_gcd.
 apply (transitive_divides ? (S m1)).
 apply divides_gcd_m.
@@ -457,7 +457,7 @@ qed.
 
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
-apply antisym_le.apply divides_to_le.simplify.apply le_n.
+apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
 apply divides_gcd_n.
 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 elim Hcut.assumption.
@@ -502,7 +502,7 @@ qed.
 
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 gcd n m = (S O).
-intros.simplify in H.change with (gcd n m = (S O)). 
+intros.unfold prime in H.change with (gcd n m = (S O)). 
 elim H.
 apply antisym_le.
 apply not_lt_to_le.
@@ -557,8 +557,8 @@ rewrite < (prime_to_gcd_SO n p).
 apply eq_minus_gcd.
 assumption.assumption.
 apply (decidable_divides n p).
-apply (trans_lt ? (S O)).simplify.apply le_n.
-simplify in H.elim H. assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
+unfold prime in H.elim H. assumption.
 qed.
 
 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
@@ -576,11 +576,11 @@ rewrite < H2 in \vdash (? ? %).
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.
-rewrite > H2.simplify.apply le_n.
+rewrite > H2.unfold lt.apply le_n.
 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 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 divides_gcd_n.
 apply (not_le_Sn_n (S O)).
 change with ((S O) < (S O)).
@@ -588,18 +588,18 @@ rewrite < H3 in \vdash (? ? %).
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.
-rewrite > H3.simplify.apply le_n.
+rewrite > H3.unfold lt.apply le_n.
 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 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 divides_gcd_n.
 apply divides_times_to_divides.
 apply prime_smallest_factor_n.
 assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 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 divides_gcd_m.
 change with (O < gcd m (n*p)).
 apply lt_O_gcd.