X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=65f61b581691cdabbdaeeb34fc7d10ac21927a93;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8475fc06aa026aacff1fd29c46c264ff25575947;hpb=30b7e65d641fe7243c4f36ed448f56360a1c5e1c;p=helm.git

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 8475fc06a..65f61b581 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -22,7 +22,7 @@ match divides_b n m with
 | false \Rightarrow 
   match p with
   [O \Rightarrow n
-  |(S q) \Rightarrow gcd_aux q n (mod m n)]].
+  |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
   
 definition gcd : nat \to nat \to nat \def
 \lambda n,m:nat.
@@ -37,28 +37,24 @@ definition gcd : nat \to nat \to nat \def
     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
 
 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
-p \divides mod m n.
+p \divides (m \mod n).
 intros.elim H1.elim H2.
-apply witness ? ? (n2 - n1*(div m n)).
+apply (witness ? ? (n2 - n1*(m / n))).
 rewrite > distr_times_minus.
 rewrite < H3.
 rewrite < assoc_times.
 rewrite < H4.
 apply sym_eq.
 apply plus_to_minus.
-rewrite > div_mod m n in \vdash (? ? %).
 rewrite > sym_times.
-apply eq_plus_to_le ? ? (mod m n).
-reflexivity.
+apply div_mod.
 assumption.
-rewrite > sym_times.
-apply div_mod.assumption.
 qed.
 
 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
-p \divides mod m n \to p \divides n \to p \divides m. 
+p \divides (m \mod n) \to p \divides n \to p \divides m. 
 intros.elim H1.elim H2.
-apply witness p m ((n1*(div m n))+n2).
+apply (witness p m ((n1*(m / n))+n2)).
 rewrite > distr_times_plus.
 rewrite < H3.
 rewrite < assoc_times.
@@ -69,30 +65,30 @@ qed.
 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
 gcd_aux p m n \divides m \land gcd_aux p m n \divides n. 
 intro.elim p.
-absurd O < n.assumption.apply le_to_not_lt.assumption.
-cut (n1 \divides m) \lor (n1 \ndivides m).
+absurd (O < n).assumption.apply le_to_not_lt.assumption.
+cut ((n1 \divides m) \lor (n1 \ndivides m)).
 change with 
-(match divides_b n1 m with
+((match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides m \land
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
 (match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides n1.
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1).
 elim Hcut.rewrite > divides_to_divides_b_true.
 simplify.
-split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
+split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
 assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
 change with 
-gcd_aux n n1 (mod m n1) \divides m \land
-gcd_aux n n1 (mod m n1) \divides n1.
-cut gcd_aux n n1 (mod m n1) \divides n1 \land
-gcd_aux n n1 (mod m n1) \divides mod m n1.
+(gcd_aux n n1 (m \mod n1) \divides m \land
+gcd_aux n n1 (m \mod n1) \divides n1).
+cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
+gcd_aux n n1 (m \mod n1) \divides mod m n1).
 elim Hcut1.
-split.apply divides_mod_to_divides ? ? n1.
+split.apply (divides_mod_to_divides ? ? n1).
 assumption.assumption.assumption.assumption.
 apply H.
-cut O \lt mod m n1 \lor O = mod m n1.
+cut (O \lt m \mod n1 \lor O = mod m n1).
 elim Hcut1.assumption.
 apply False_ind.apply H4.apply mod_O_to_divides.
 assumption.apply sym_eq.assumption.
@@ -100,18 +96,18 @@ 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 (trans_le ? n1).
+change with (m \mod n1 < n1).
 apply lt_mod_m_m.assumption.assumption.
 assumption.assumption.
-apply decidable_divides n1 m.assumption.
+apply (decidable_divides n1 m).assumption.
 qed.
 
 theorem divides_gcd_nm: \forall n,m.
 gcd n m \divides m \land gcd n m \divides n.
 intros.
 change with
-match leb n m with
+(match leb n m with
   [ true \Rightarrow 
     match n with 
     [ O \Rightarrow m
@@ -119,7 +115,7 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
 \land
 match leb n m with
   [ true \Rightarrow 
@@ -129,88 +125,88 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n. 
-apply leb_elim n m.
-apply nat_case1 n.
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n). 
+apply (leb_elim n m).
+apply (nat_case1 n).
 simplify.intros.split.
-apply witness m m (S O).apply times_n_SO.
-apply witness m O O.apply times_n_O.
+apply (witness m m (S O)).apply times_n_SO.
+apply (witness m O O).apply times_n_O.
 intros.change with
-gcd_aux (S m1) m (S m1) \divides m
+(gcd_aux (S m1) m (S m1) \divides m
 \land 
-gcd_aux (S m1) m (S m1) \divides (S m1).
+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.
+apply (nat_case1 m).
 simplify.intros.split.
-apply witness n O O.apply times_n_O.
-apply witness n n (S O).apply times_n_SO.
+apply (witness n O O).apply times_n_O.
+apply (witness n n (S O)).apply times_n_SO.
 intros.change with
-gcd_aux (S m1) n (S m1) \divides (S m1)
+(gcd_aux (S m1) n (S m1) \divides (S m1)
 \land 
-gcd_aux (S m1) n (S m1) \divides n.
-cut gcd_aux (S m1) n (S m1) \divides n
+gcd_aux (S m1) n (S m1) \divides n).
+cut (gcd_aux (S m1) n (S m1) \divides n
 \land 
-gcd_aux (S m1) n (S m1) \divides S m1.
+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.
-rewrite > H1.apply trans_le ? (S n).
+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.
 
 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
 intros. 
-exact proj2  ? ? (divides_gcd_nm n m).
+exact (proj2  ? ? (divides_gcd_nm n m)).
 qed.
 
 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
 intros. 
-exact proj1 ? ? (divides_gcd_nm n m).
+exact (proj1 ? ? (divides_gcd_nm n m)).
 qed.
 
 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 d \divides m \to d \divides n \to d \divides gcd_aux p m n. 
 intro.elim p.
-absurd O < n.assumption.apply le_to_not_lt.assumption.
+absurd (O < n).assumption.apply le_to_not_lt.assumption.
 change with
-d \divides
+(d \divides
 (match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]).
-cut n1 \divides m \lor n1 \ndivides m.
+| false \Rightarrow gcd_aux n n1 (m \mod n1)])).
+cut (n1 \divides m \lor n1 \ndivides m).
 elim Hcut.
 rewrite > divides_to_divides_b_true.
 simplify.assumption.
 assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
-change with d \divides gcd_aux n n1 (mod m n1).
+change with (d \divides gcd_aux n n1 (m \mod n1)).
 apply H.
-cut O \lt mod m n1 \lor O = mod m n1.
+cut (O \lt m \mod n1 \lor O = m \mod n1).
 elim Hcut1.assumption.
-absurd n1 \divides m.apply mod_O_to_divides.
+absurd (n1 \divides m).apply mod_O_to_divides.
 assumption.apply sym_eq.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 (trans_le ? n1).
+change with (m \mod 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 (decidable_divides n1 m).assumption.
 qed.
 
 theorem divides_d_gcd: \forall m,n,d. 
 d \divides m \to d \divides n \to d \divides gcd n m. 
 intros.
 change with
-d \divides
+(d \divides
 match leb n m with
   [ true \Rightarrow 
     match n with 
@@ -219,19 +215,19 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
-apply leb_elim n m.
-apply nat_case1 n.simplify.intros.assumption.
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+apply (leb_elim n m).
+apply (nat_case1 n).simplify.intros.assumption.
 intros.
-change with d \divides gcd_aux (S m1) m (S m1).
+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.
+apply (nat_case1 m).simplify.intros.assumption.
 intros.
-change with d \divides gcd_aux (S m1) n (S m1).
+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.
@@ -240,49 +236,49 @@ theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 intro.
 elim p.
-absurd O < n.assumption.apply le_to_not_lt.assumption.
-cut O < m.
-cut n1 \divides m \lor  n1 \ndivides m.
+absurd (O < n).assumption.apply le_to_not_lt.assumption.
+cut (O < m).
+cut (n1 \divides m \lor  n1 \ndivides m).
 change with
-\exists a,b.
+(\exists a,b.
 a*n1 - b*m = match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)]
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]
 \lor 
 b*m - a*n1 = match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)].
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]).
 elim Hcut1.
 rewrite > divides_to_divides_b_true.
 simplify.
-apply ex_intro ? ? (S O).
-apply ex_intro ? ? O.
+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
-\exists a,b.
-a*n1 - b*m = gcd_aux n n1 (mod m n1)
+(\exists a,b.
+a*n1 - b*m = gcd_aux n n1 (m \mod n1)
 \lor 
-b*m - a*n1 = gcd_aux n n1 (mod m n1).
+b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
 cut 
-\exists a,b.
-a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
+(\exists a,b.
+a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
 \lor
-b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
+b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
 elim Hcut2.elim H5.elim H6.
 (* first case *)
 rewrite < H7.
-apply ex_intro ? ? (a1+a*(div m n1)).
-apply ex_intro ? ? a.
+apply (ex_intro ? ? (a1+a*(m / n1))).
+apply (ex_intro ? ? a).
 right.
 rewrite < sym_plus.
-rewrite < sym_times n1.
+rewrite < (sym_times n1).
 rewrite > distr_times_plus.
-rewrite > sym_times n1.
-rewrite > sym_times n1.
-rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
+rewrite > (sym_times n1).
+rewrite > (sym_times n1).
+rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
 rewrite > assoc_times.
 rewrite < sym_plus.
 rewrite > distr_times_plus.
@@ -294,14 +290,15 @@ apply le_n.
 assumption.
 (* second case *)
 rewrite < H7.
-apply ex_intro ? ? (a1+a*(div m n1)).
-apply ex_intro ? ? a.
+apply (ex_intro ? ? (a1+a*(m / n1))).
+apply (ex_intro ? ? a).
 left.
+(* clear Hcut2.clear H5.clear H6.clear H. *)
 rewrite > sym_times.
 rewrite > distr_times_plus.
 rewrite > sym_times.
-rewrite > sym_times n1.
-rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
+rewrite > (sym_times n1).
+rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
 rewrite > distr_times_plus.
 rewrite > assoc_times.
 rewrite < eq_minus_minus_minus_plus.
@@ -310,91 +307,70 @@ rewrite < plus_minus.
 rewrite < minus_n_n.reflexivity.
 apply le_n.
 assumption.
-apply H n1 (mod m n1).
-cut O \lt mod m n1 \lor O = mod m n1.
+apply (H n1 (m \mod n1)).
+cut (O \lt m \mod n1 \lor O = m \mod n1).
 elim Hcut2.assumption. 
-absurd n1 \divides m.apply mod_O_to_divides.
+absurd (n1 \divides m).apply mod_O_to_divides.
 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 (trans_le ? n1).
+change with (m \mod n1 < n1).
 apply lt_mod_m_m.
 assumption.assumption.assumption.assumption.
-apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.assumption.
+apply (decidable_divides n1 m).assumption.
+apply (lt_to_le_to_lt ? n1).assumption.assumption.
 qed.
 
 theorem eq_minus_gcd:
  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 intros.
-change with
-\exists a,b.
-a*n - b*m = 
-match leb n m with
-  [ true \Rightarrow 
-    match n with 
-    [ O \Rightarrow m
-    | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
-  | false \Rightarrow 
-    match m with 
-    [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
-\lor b*m - a*n = 
-match leb n m with
-  [ true \Rightarrow 
-    match n with 
-    [ O \Rightarrow m
-    | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
-  | false \Rightarrow 
-    match m with 
-    [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
-apply leb_elim n m.
-apply nat_case1 n.
+unfold gcd.
+apply (leb_elim n m).
+apply (nat_case1 n).
 simplify.intros.
-apply ex_intro ? ? O.
-apply ex_intro ? ? (S O).
+apply (ex_intro ? ? O).
+apply (ex_intro ? ? (S O)).
 right.simplify.
 rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
 intros.
 change with 
-\exists a,b.
+(\exists a,b.
 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)).
+\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.
+apply (nat_case1 m).
 simplify.intros.
-apply ex_intro ? ? (S O).
-apply ex_intro ? ? O.
+apply (ex_intro ? ? (S O)).
+apply (ex_intro ? ? O).
 left.simplify.
 rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
 intros.
 change with 
-\exists a,b.
+(\exists a,b.
 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) 
-\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
 cut 
-\exists a,b.
+(\exists a,b.
 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 \lor
-b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
 elim Hcut.elim H2.elim H3.
-apply ex_intro ? ? a1.
-apply ex_intro ? ? a.
+apply (ex_intro ? ? a1).
+apply (ex_intro ? ? a).
 right.assumption.
-apply ex_intro ? ? a1.
-apply ex_intro ? ? a.
+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.
@@ -407,20 +383,30 @@ qed.
 
 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 m = O \land n = O.
-intros.cut O \divides n \land O \divides m.
+intros.cut (O \divides n \land O \divides m).
 elim Hcut.elim H2.split.
 assumption.elim H1.assumption.
 rewrite < H.
 apply divides_gcd_nm.
 qed.
 
+theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
+intros.
+apply (nat_case1 (gcd m n)).
+intros.
+generalize in match (gcd_O_to_eq_O m n H1).
+intros.elim H2.
+rewrite < H4 in \vdash (? ? %).assumption.
+intros.unfold lt.apply le_S_S.apply le_O_n.
+qed.
+
 theorem symmetric_gcd: symmetric nat gcd.
 change with 
-\forall n,m:nat. gcd n m = gcd m n.
+(\forall n,m:nat. gcd n m = gcd m n).
 intros.
-cut O < (gcd n m) \lor O = (gcd n m).
+cut (O < (gcd n m) \lor O = (gcd n m)).
 elim Hcut.
-cut O < (gcd m n) \lor O = (gcd m n).
+cut (O < (gcd m n) \lor O = (gcd m n)).
 elim Hcut1.
 apply antisym_le.
 apply divides_to_le.assumption.
@@ -428,12 +414,12 @@ apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 apply divides_to_le.assumption.
 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 rewrite < H1.
-cut m=O \land n=O.
+cut (m=O \land n=O).
 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 rewrite < H.
-cut n=O \land m=O.
+cut (n=O \land m=O).
 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
@@ -442,35 +428,93 @@ qed.
 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 symmetric_gcd.
 
+theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
+intros.
+apply (nat_case n).reflexivity.
+intro.
+apply divides_to_le.
+apply lt_O_gcd.
+rewrite > (times_n_O O).
+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.
+apply (witness ? ? p).reflexivity.
+apply divides_gcd_n.
+qed.
+
+theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to 
+gcd m (n*p) = (S O) \to gcd m n = (S O).
+intros.
+apply antisymmetric_le.
+rewrite < H2.
+apply le_gcd_times.assumption.
+change with (O < gcd m n). 
+apply lt_O_gcd.assumption.
+qed.
+
+(* for the "converse" of the previous result see the end  of this development *)
+
 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.
+cut (O < gcd (S O) n \lor O = gcd (S O) n).
 elim Hcut.assumption.
 apply False_ind.
-apply not_eq_O_S O.
-cut (S O)=O \land n=O.
+apply (not_eq_O_S O).
+cut ((S O)=O \land n=O).
 elim Hcut1.apply sym_eq.assumption.
 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
+theorem divides_gcd_mod: \forall m,n:nat. O < n \to
+divides (gcd m n) (gcd n (m \mod n)).
+intros.
+apply divides_d_gcd.
+apply divides_mod.assumption.
+apply divides_gcd_n.
+apply divides_gcd_m.
+apply divides_gcd_m.
+qed.
+
+theorem divides_mod_gcd: \forall m,n:nat. O < n \to
+divides (gcd n (m \mod n)) (gcd m n) .
+intros.
+apply divides_d_gcd.
+apply divides_gcd_n.
+apply (divides_mod_to_divides ? ? n).
+assumption.
+apply divides_gcd_m.
+apply divides_gcd_n.
+qed.
+
+theorem gcd_mod: \forall m,n:nat. O < n \to
+(gcd n (m \mod n)) = (gcd m n) .
+intros.
+apply antisymmetric_divides.
+apply divides_mod_gcd.assumption.
+apply divides_gcd_mod.assumption.
+qed.
+
+(* gcd and primes *)
+
 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.
-change with (S (S O)) \le gcd n m \to False.intro.
-apply H1.rewrite < H3 (gcd n m).
+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.
+cut (O < gcd n m \lor O = gcd n m).
 elim Hcut.assumption.
 apply False_ind.
-apply not_le_Sn_O (S O).
-cut n=O \land m=O.
+apply (not_le_Sn_O (S O)).
+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.
@@ -479,40 +523,86 @@ qed.
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 n \divides p \lor n \divides q.
 intros.
-cut n \divides p \lor n \ndivides p.
+cut (n \divides p \lor n \ndivides p).
 elim Hcut.
 left.assumption.
 right.
-cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
+cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O)).
 elim Hcut1.elim H3.elim H4.
 (* first case *)
-rewrite > times_n_SO q.rewrite < H5.
+rewrite > (times_n_SO q).rewrite < H5.
 rewrite > distr_times_minus.
-rewrite > sym_times q (a1*p).
-rewrite > assoc_times a1.
+rewrite > (sym_times q (a1*p)).
+rewrite > (assoc_times a1).
 elim H1.rewrite > H6.
-rewrite < sym_times n.rewrite < assoc_times.
-rewrite > sym_times q.rewrite > assoc_times.
-rewrite < assoc_times a1.rewrite < sym_times n.
-rewrite > assoc_times n.
+rewrite < (sym_times n).rewrite < assoc_times.
+rewrite > (sym_times q).rewrite > assoc_times.
+rewrite < (assoc_times a1).rewrite < (sym_times n).
+rewrite > (assoc_times n).
 rewrite < distr_times_minus.
-apply witness ? ? (q*a-a1*n2).reflexivity.
+apply (witness ? ? (q*a-a1*n2)).reflexivity.
 (* second case *)
-rewrite > times_n_SO q.rewrite < H5.
+rewrite > (times_n_SO q).rewrite < H5.
 rewrite > distr_times_minus.
-rewrite > sym_times q (a1*p).
-rewrite > assoc_times a1.
+rewrite > (sym_times q (a1*p)).
+rewrite > (assoc_times a1).
 elim H1.rewrite > H6.
 rewrite < sym_times.rewrite > assoc_times.
-rewrite < assoc_times q.
-rewrite < sym_times n.
+rewrite < (assoc_times q).
+rewrite < (sym_times n).
 rewrite < distr_times_minus.
-apply witness ? ? (n2*a1-q*a).reflexivity.
+apply (witness ? ? (n2*a1-q*a)).reflexivity.
 (* end second case *)
-rewrite < prime_to_gcd_SO n p.
+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 (decidable_divides n p).
+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
+gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
+intros.
+apply antisymmetric_le.
+apply not_lt_to_le.
+unfold Not.intro.
+cut (divides (smallest_factor (gcd m (n*p))) n \lor 
+     divides (smallest_factor (gcd m (n*p))) p).
+elim Hcut.
+apply (not_le_Sn_n (S O)).
+change with ((S O) < (S O)).
+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.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)). unfold lt. apply le_n. assumption.
+apply divides_gcd_n.
+apply (not_le_Sn_n (S O)).
+change with ((S O) < (S O)).
+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.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)). 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)).unfold lt. apply le_n. assumption.
+apply divides_gcd_m.
+change with (O < gcd m (n*p)).
+apply lt_O_gcd.
+rewrite > (times_n_O O).
+apply lt_times.assumption.assumption.
 qed.