added a function to reorder the metasenv.

[helm.git] / helm / matita / library / nat / gcd.ma

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 5a2fd4647e80bf342b650e0825c3333568b55047..921d8853e87a6cf03fee66f79bdfb4f6a1e0bfc2 100644 (file)
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -51,8 +51,9 @@ rewrite > div_mod m n in \vdash (? ? %).
 rewrite > sym_times.
 apply eq_plus_to_le ? ? (mod m n).
 reflexivity.
+assumption.
 rewrite > sym_times.
-apply div_mod.assumption. assumption.
+apply div_mod.assumption.
 qed.
 
 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
@@ -83,6 +84,7 @@ change with
 elim Hcut.rewrite > divides_to_divides_b_true.
 simplify.
 split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
+assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
 change with 
 (divides (gcd_aux n n1 (mod m n1)) m) \land
@@ -104,10 +106,8 @@ apply le_S_S_to_le.
 apply trans_le ? n1.
 change with mod m n1 < n1.
 apply lt_mod_m_m.assumption.assumption.
-apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.reflexivity.
-assumption.
 assumption.assumption.
+apply decidable_divides n1 m.assumption.
 qed.
 
 theorem divides_gcd_nm: \forall n,m.
@@ -192,6 +192,7 @@ cut divides n1 m \lor \not (divides n1 m).
 elim Hcut.
 rewrite > divides_to_divides_b_true.
 simplify.assumption.
+assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
 change with divides d (gcd_aux n n1 (mod m n1)).
 apply H.
@@ -208,9 +209,8 @@ change with mod m n1 < n1.
 apply lt_mod_m_m.assumption.assumption.
 assumption.
 apply divides_mod.assumption.assumption.assumption.
+assumption.assumption.
 apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.reflexivity.
-assumption.assumption.assumption.
 qed.
 
 theorem divides_d_gcd: \forall m,n,d. 
@@ -267,6 +267,7 @@ apply ex_intro ? ? (S O).
 apply ex_intro ? ? O.
 left.simplify.rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
+assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
 change with
 ex nat (\lambda a. ex nat (\lambda b.
@@ -297,6 +298,8 @@ rewrite < eq_minus_minus_minus_plus.
 rewrite < sym_plus.
 rewrite < plus_minus.
 rewrite < minus_n_n.reflexivity.
+apply le_n.
+assumption.
 (* second case *)
 rewrite < H7.
 apply ex_intro ? ? (a1+a*(div m n1)).
@@ -313,25 +316,24 @@ rewrite < eq_minus_minus_minus_plus.
 rewrite < sym_plus.
 rewrite < plus_minus.
 rewrite < minus_n_n.reflexivity.
-(* end second case *)
+apply le_n.
+assumption.
 apply H n1 (mod m n1).
-(* a lot of trivialities left *)
 cut O \lt mod m n1 \lor O = mod m n1.
-elim Hcut2.assumption.
+elim Hcut2.assumption. 
 absurd divides n1 m.apply mod_O_to_divides.
-assumption.apply sym_eq.assumption.assumption.
+assumption.
+symmetry.assumption.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 apply lt_to_le.
 apply lt_mod_m_m.assumption.
 apply le_S_S_to_le.
 apply trans_le ? n1.
 change with mod m n1 < n1.
-apply lt_mod_m_m.assumption.assumption.
+apply lt_mod_m_m.
+assumption.assumption.assumption.assumption.
 apply decidable_divides n1 m.assumption.
 apply lt_to_le_to_lt ? n1.assumption.assumption.
-assumption.assumption.assumption.assumption.assumption.
-apply le_n.assumption.
-apply le_n.
 qed.
 
 theorem eq_minus_gcd: \forall m,n.
@@ -473,6 +475,7 @@ apply not_lt_to_le.
 change with (S (S O)) \le gcd n m \to False.intro.
 apply H1.rewrite < H3 (gcd n m).
 apply divides_gcd_m.
+apply divides_gcd_n.assumption.
 cut O < gcd n m \lor O = gcd n m.
 elim Hcut.assumption.
 apply False_ind.
@@ -481,7 +484,6 @@ cut n=O \land m=O.
 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
-apply divides_gcd_n.assumption.
 qed.
 
 (* esempio di sfarfallalmento !!! *)
@@ -532,8 +534,8 @@ apply witness ? ? (n2*a1-q*a).reflexivity.
 (* end second case *)
 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.
-assumption.assumption.
 qed.