completed use of \mod and / notation

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

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 43fe7f649ba4ac93223e4f213fa77369cd7a582a..be3660187d7d1b126c7c35adf04554fa09b65ea4 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -33,7 +33,7 @@ exact witness x x (S O) (times_n_SO x).
 qed.
 
 theorem divides_to_div_mod_spec :
-\forall n,m. O < n \to n \divides m \to div_mod_spec m n (div m n) O.
+\forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
 intros.elim H1.rewrite > H2.
 constructor 1.assumption.
 apply lt_O_n_elim n H.intros.
@@ -50,17 +50,17 @@ rewrite > plus_n_O (p*n).assumption.
 qed.
 
 theorem divides_to_mod_O:
-\forall n,m. O < n \to n \divides m \to (mod m n) = O.
-intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O.
+\forall n,m. O < n \to n \divides m \to (m \mod n) = O.
+intros.apply div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O.
 apply div_mod_spec_div_mod.assumption.
 apply divides_to_div_mod_spec.assumption.assumption.
 qed.
 
 theorem mod_O_to_divides:
-\forall n,m. O< n \to (mod m n) = O \to  n \divides m.
+\forall n,m. O< n \to (m \mod n) = O \to  n \divides m.
 intros.
-apply witness n m (div m n).
-rewrite > plus_n_O (n*div m n).
+apply witness n m (m / n).
+rewrite > plus_n_O (n * (m / n)).
 rewrite < H1.
 rewrite < sym_times.
 (* Andrea: perche' hint non lo trova ?*)
@@ -141,7 +141,7 @@ qed.
 
 (* boolean divides *)
 definition divides_b : nat \to nat \to bool \def
-\lambda n,m :nat. (eqb (mod m n) O).
+\lambda n,m :nat. (eqb (m \mod n) O).
   
 theorem divides_b_to_Prop :
 \forall n,m:nat. O < n \to
@@ -150,7 +150,7 @@ match divides_b n m with
 | false \Rightarrow n \ndivides m].
 intros.
 change with 
-match eqb (mod m n) O with
+match eqb (m \mod n) O with
 [ true \Rightarrow n \divides m
 | false \Rightarrow n \ndivides m].
 apply eqb_elim.
@@ -233,8 +233,8 @@ apply inj_S.assumption.
 qed.
 
 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. 
-i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O).
-intros.cut mod (pi n f) (f i) = O.
+i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
+intros.cut (pi n f) \mod (f i) = O.
 rewrite < Hcut.
 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
 rewrite > Hcut.assumption.
@@ -259,8 +259,8 @@ apply witness ? ? n1!.reflexivity.
 qed.
 
 theorem mod_S_fact: \forall n,i:nat. 
-(S O) < i \to i \le n \to mod (S n!) i = (S O).
-intros.cut mod n! i = O.
+(S O) < i \to i \le n \to (S n!) \mod i = (S O).
+intros.cut n! \mod i = O.
 rewrite < Hcut.
 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
 rewrite > Hcut.assumption.
@@ -274,7 +274,7 @@ theorem not_divides_S_fact: \forall n,i:nat.
 intros.
 apply divides_b_false_to_not_divides.
 apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb (mod (S n!) i) O) = false.
+change with (eqb ((S n!) \mod i) O) = false.
 rewrite > mod_S_fact.simplify.reflexivity.
 assumption.assumption.
 qed.
@@ -300,7 +300,7 @@ match n with
 | (S p) \Rightarrow 
   match p with
   [ O \Rightarrow (S O)
-  | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]].
+  | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
 
 (* it works ! 
 theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
@@ -322,7 +322,7 @@ apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
 intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
 intros.
 change with 
-S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)).
+S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O)).
 apply lt_to_le_to_lt ? (S (S O)).
 apply le_n (S(S O)).
 cut (S(S O)) = (S(S m1)) - m1.
@@ -353,8 +353,8 @@ intros.
 apply divides_b_true_to_divides.
 apply lt_O_smallest_factor ? H.
 change with 
-eqb (mod (S(S m1)) (min_aux m1 (S(S m1)) 
-  (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true.
+eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) 
+  (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true.
 apply f_min_aux_true.
 apply ex_intro nat ? (S(S m1)).
 split.split.
@@ -382,9 +382,9 @@ intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
 intros.
 apply divides_b_false_to_not_divides.
 apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb (mod (S(S m1)) i) O) = false.
+change with (eqb ((S(S m1)) \mod i) O) = false.
 apply lt_min_aux_to_false 
-(\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i.
+(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i.
 cut (S(S O)) = (S(S m1)-m1).
 rewrite < Hcut.exact H1.
 apply sym_eq. apply plus_to_minus.