completed use of \mod and / notation

[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 99c97b09add8d506bc1566c5250da6fd3b76969f..36c7a96597fef1f5b83169d5b08af8c842ba30b4 100644 (file)
--- 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,9 +37,9 @@ 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.
@@ -48,7 +48,7 @@ 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).
+apply eq_plus_to_le ? ? (m \mod n).
 reflexivity.
 assumption.
 rewrite > sym_times.
@@ -56,9 +56,9 @@ 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.
@@ -74,25 +74,25 @@ cut (n1 \divides m) \lor (n1 \ndivides m).
 change 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.
 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.
 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.
@@ -101,7 +101,7 @@ 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.
+change with m \mod n1 < n1.
 apply lt_mod_m_m.assumption.assumption.
 assumption.assumption.
 apply decidable_divides n1 m.assumption.
@@ -180,16 +180,16 @@ change with
 d \divides
 (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)]).
 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.
 assumption.apply sym_eq.assumption.assumption.
@@ -198,7 +198,7 @@ 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.
+change with m \mod n1 < n1.
 apply lt_mod_m_m.assumption.assumption.
 assumption.
 apply divides_mod.assumption.assumption.assumption.
@@ -247,11 +247,11 @@ change with
 \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.
@@ -263,18 +263,18 @@ 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)
+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)
+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 ? ? (a1+a*(m / n1)).
 apply ex_intro ? ? a.
 right.
 rewrite < sym_plus.
@@ -294,7 +294,7 @@ apply le_n.
 assumption.
 (* second case *)
 rewrite < H7.
-apply ex_intro ? ? (a1+a*(div m n1)).
+apply ex_intro ? ? (a1+a*(m / n1)).
 apply ex_intro ? ? a.
 left.
 (* clear Hcut2.clear H5.clear H6.clear H. *)
@@ -311,8 +311,8 @@ 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.
 assumption.
@@ -322,7 +322,7 @@ 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.
+change with m \mod n1 < n1.
 apply lt_mod_m_m.
 assumption.assumption.assumption.assumption.
 apply decidable_divides n1 m.assumption.