From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Sep 2005 12:56:30 +0000 (+0000)
Subject: completed use of \mod and / notation
X-Git-Tag: V_0_7_2_3~300
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63e834c4fbcb3d015f418989ccd6d2fc8c3dd9ab;p=helm.git

completed use of \mod and / notation
---

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index f9f0289a0..fc51b32ff 100644
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -21,14 +21,14 @@ include "nat/nth_prime.ma".
 (* the following factorization algorithm looks for the largest prime
    factor. *)
 definition max_prime_factor \def \lambda n:nat.
-(max n (\lambda p:nat.eqb (mod n (nth_prime p)) O)).
+(max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
 
 (* max_prime_factor is indeed a factor *)
 theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to
 nth_prime (max_prime_factor n) \divides n.
 intros.apply divides_b_true_to_divides.
 apply lt_O_nth_prime_n.
-apply f_max_true  (\lambda p:nat.eqb (mod n (nth_prime p)) O) n.
+apply f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n.
 cut \exists i. nth_prime i = smallest_factor n.
 elim Hcut.
 apply ex_intro nat ? a.
@@ -51,8 +51,8 @@ qed.
 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to 
 max_prime_factor n \le max_prime_factor m.
 intros.change with
-(max n (\lambda p:nat.eqb (mod n (nth_prime p)) O)) \le
-(max m (\lambda p:nat.eqb (mod m (nth_prime p)) O)).
+(max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le
+(max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O)).
 apply f_m_to_le_max.
 apply trans_le ? n.
 apply le_max_n.apply divides_to_le.assumption.assumption.
@@ -87,7 +87,7 @@ apply divides_max_prime_factor_n.
 assumption.
 change with nth_prime (max_prime_factor n) \divides r \to False.
 intro.
-cut mod r (nth_prime (max_prime_factor n)) \neq O.
+cut r \mod (nth_prime (max_prime_factor n)) \neq O.
 apply Hcut1.apply divides_to_mod_O.
 apply lt_O_nth_prime_n.assumption.
 apply p_ord_aux_to_not_mod_O n n ? q r.
@@ -147,7 +147,7 @@ definition factorize : nat \to nat_fact_all \def \lambda n:nat.
       match n1 with
       [ O \Rightarrow nfa_one
     | (S n2) \Rightarrow 
-      let p \def (max (S(S n2)) (\lambda p:nat.eqb (mod (S(S n2)) (nth_prime p)) O)) in
+      let p \def (max (S(S n2)) (\lambda p:nat.eqb ((S(S n2)) \mod (nth_prime p)) O)) in
       match p_ord (S(S n2)) (nth_prime p) with
       [ (pair q r) \Rightarrow 
            nfa_proper (factorize_aux p r (nf_last (pred q)))]]].
@@ -275,7 +275,7 @@ intro.
 apply nat_case n.reflexivity.
 intro.apply nat_case m.reflexivity.
 intro.change with  
-let p \def (max (S(S m1)) (\lambda p:nat.eqb (mod (S(S m1)) (nth_prime p)) O)) in
+let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
 defactorize (match p_ord (S(S m1)) (nth_prime p) with
 [ (pair q r) \Rightarrow 
    nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)).
diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 99c97b09a..36c7a9659 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,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.
diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index a2e7f6109..ce66decaa 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -162,11 +162,11 @@ qed.
 
 (* div *) 
 
-theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m. 
+theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
 intros 4.apply lt_O_n_elim m H.intros.
 apply lt_times_to_lt_r m1.
 rewrite < times_n_O.
-rewrite > plus_n_O ((S m1)*(div n (S m1))).
+rewrite > plus_n_O ((S m1)*(n / (S m1))).
 rewrite < H2.
 rewrite < sym_times.
 rewrite < div_mod.
@@ -175,13 +175,13 @@ assumption.
 simplify.apply le_S_S.apply le_O_n.
 qed.
 
-theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to div n m \lt n.
+theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 intros.
-apply nat_case1 (div n m).intro.
+apply nat_case1 (n / m).intro.
 assumption.intros.rewrite < H2.
 rewrite > (div_mod n m) in \vdash (? ? %).
-apply lt_to_le_to_lt ? ((div n m)*m).
-apply lt_to_le_to_lt ? ((div n m)*(S (S O))).
+apply lt_to_le_to_lt ? ((n / m)*m).
+apply lt_to_le_to_lt ? ((n / m)*(S (S O))).
 rewrite < sym_times.
 rewrite > H2.
 simplify.
diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma
index 7b246be0e..d0e2b98f0 100644
--- a/helm/matita/library/nat/ord.ma
+++ b/helm/matita/library/nat/ord.ma
@@ -22,12 +22,12 @@ include "nat/primes.ma".
 (* this definition of log is based on pairs, with a remainder *)
 
 let rec p_ord_aux p n m \def
-  match (mod n m) with
+  match n \mod m with
   [ O \Rightarrow 
     match p with
       [ O \Rightarrow pair nat nat O n
       | (S p) \Rightarrow 
-       match (p_ord_aux p (div n m) m) with
+       match (p_ord_aux p (n / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]]
   | (S a) \Rightarrow pair nat nat O n].
   
@@ -41,36 +41,36 @@ intro.
 elim p.
 change with 
 match (
-match (mod n m) with
+match n \mod m with
   [ O \Rightarrow pair nat nat O n
   | (S a) \Rightarrow pair nat nat O n] )
 with
   [ (pair q r) \Rightarrow n = m \sup q * r ].
-apply nat_case (mod n m).
+apply nat_case (n \mod m).
 simplify.apply plus_n_O.
 intros.
 simplify.apply plus_n_O. 
 change with 
 match (
-match (mod n1 m) with
+match n1 \mod m with
   [ O \Rightarrow 
-     match (p_ord_aux n (div n1 m) m) with
+     match (p_ord_aux n (n1 / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O n1] )
 with
   [ (pair q r) \Rightarrow n1 = m \sup q * r].
-apply nat_case1 (mod n1 m).intro.
+apply nat_case1 (n1 \mod m).intro.
 change with 
 match (
- match (p_ord_aux n (div n1 m) m) with
+ match (p_ord_aux n (n1 / m) m) with
    [ (pair q r) \Rightarrow pair nat nat (S q) r])
 with
   [ (pair q r) \Rightarrow n1 = m \sup q * r].
-generalize in match (H (div n1 m) m).
-elim p_ord_aux n (div n1 m) m.
+generalize in match (H (n1 / m) m).
+elim p_ord_aux n (n1 / m) m.
 simplify.
 rewrite > assoc_times.
-rewrite < H3.rewrite > plus_n_O (m*(div n1 m)).
+rewrite < H3.rewrite > plus_n_O (m*(n1 / m)).
 rewrite < H2.
 rewrite > sym_times.
 rewrite < div_mod.reflexivity.
@@ -89,7 +89,7 @@ apply p_ord_aux_to_Prop.
 assumption.
 qed.
 (* questo va spostato in primes1.ma *)
-theorem p_ord_exp: \forall n,m,i. O < m \to mod n m \neq O \to
+theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
 intros 5.
 elim i.
@@ -97,21 +97,21 @@ simplify.
 rewrite < plus_n_O.
 apply nat_case p.
 change with
- match (mod n m) with
+ match n \mod m with
   [ O \Rightarrow pair nat nat O n
   | (S a) \Rightarrow pair nat nat O n]
   = pair nat nat O n.
-elim (mod n m).simplify.reflexivity.simplify.reflexivity.
+elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
 intro.
 change with
- match (mod n m) with
+ match n \mod m with
   [ O \Rightarrow 
-       match (p_ord_aux m1 (div n m) m) with
+       match (p_ord_aux m1 (n / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O n]
   = pair nat nat O n.
-cut O < mod n m \lor O = mod n m.
-elim Hcut.apply lt_O_n_elim (mod n m) H3.
+cut O < n \mod m \lor O = n \mod m.
+elim Hcut.apply lt_O_n_elim (n \mod m) H3.
 intros. simplify.reflexivity.
 apply False_ind.
 apply H1.apply sym_eq.assumption.
@@ -120,24 +120,24 @@ generalize in match H3.
 apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
 intros.
 change with
- match (mod (m \sup (S n1) *n) m) with
+ match ((m \sup (S n1) *n) \mod m) with
   [ O \Rightarrow 
-       match (p_ord_aux m1 (div (m \sup (S n1) *n) m) m) with
+       match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
   = pair nat nat (S n1) n.
-cut (mod (m \sup (S n1)*n) m) = O.
+cut ((m \sup (S n1)*n) \mod m) = O.
 rewrite > Hcut.
 change with
-match (p_ord_aux m1 (div (m \sup (S n1)*n) m) m) with
+match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r] 
   = pair nat nat (S n1) n. 
-cut div (m \sup (S n1) *n) m = m \sup n1 *n.
+cut (m \sup (S n1) *n) / m = m \sup n1 *n.
 rewrite > Hcut1.
 rewrite > H2 m1. simplify.reflexivity.
 apply le_S_S_to_le.assumption.
 (* div_exp *)
-change with div (m* m \sup n1 *n) m = m \sup n1 * n.
+change with (m* m \sup n1 *n) / m = m \sup n1 * n.
 rewrite > assoc_times.
 apply lt_O_n_elim m H.
 intro.apply div_times.
@@ -150,30 +150,30 @@ qed.
 
 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
   match p_ord_aux p n m with
-  [ (pair q r) \Rightarrow mod r m \neq O].
+  [ (pair q r) \Rightarrow r \mod m \neq O].
 intro.elim p.absurd O < n.assumption.
 apply le_to_not_lt.assumption.
 change with
 match 
-  (match (mod n1 m) with
+  (match n1 \mod m with
     [ O \Rightarrow 
-        match (p_ord_aux n(div n1 m) m) with
+        match (p_ord_aux n(n1 / m) m) with
         [ (pair q r) \Rightarrow pair nat nat (S q) r]
     | (S a) \Rightarrow pair nat nat O n1])
 with
-  [ (pair q r) \Rightarrow mod r m \neq O].
-apply nat_case1 (mod n1 m).intro.
-generalize in match (H (div n1 m) m).
-elim (p_ord_aux n (div n1 m) m).
+  [ (pair q r) \Rightarrow r \mod m \neq O].
+apply nat_case1 (n1 \mod m).intro.
+generalize in match (H (n1 / m) m).
+elim (p_ord_aux n (n1 / m) m).
 apply H5.assumption.
 apply eq_mod_O_to_lt_O_div.
 apply trans_lt ? (S O).simplify.apply le_n.
 assumption.assumption.assumption.
 apply le_S_S_to_le.
-apply trans_le ? n1.change with div n1 m < n1.
+apply trans_le ? n1.change with n1 / m < n1.
 apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
-change with mod n1 m \neq O.
+change with n1 \mod m \neq O.
 rewrite > H4.
 (* Andrea: META NOT FOUND !!!  
 rewrite > sym_eq. *)
@@ -183,11 +183,11 @@ rewrite > H5.reflexivity.
 qed.
 
 theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
- pair nat nat q r = p_ord_aux p n m \to mod r m \neq O.
+ pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
 intros.
 change with 
   match (pair nat nat q r) with
-  [ (pair q r) \Rightarrow mod r m \neq O].
+  [ (pair q r) \Rightarrow r \mod m \neq O].
 rewrite > H3. 
 apply p_ord_aux_to_Prop1.
 assumption.assumption.assumption.
diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 43fe7f649..be3660187 100644
--- 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.
diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma
index 37fcbd21f..3ec61ee4a 100644
--- a/helm/matita/library/nat/primes1.ma
+++ b/helm/matita/library/nat/primes1.ma
@@ -19,11 +19,11 @@ include "nat/primes.ma".
 
 (* p is just an upper bound, acc is an accumulator *)
 let rec n_divides_aux p n m acc \def
-  match (mod n m) with
+  match n \mod m with
   [ O \Rightarrow 
     match p with
       [ O \Rightarrow pair nat nat acc n
-      | (S p) \Rightarrow n_divides_aux p (div n m) m (S acc)]
+      | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
   | (S a) \Rightarrow pair nat nat acc n].
 
 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
@@ -34,5 +34,5 @@ theorem n_divides_to_Prop: \forall n,m,p,a.
   match n_divides_aux p n m a with
   [ (pair q r) \Rightarrow n = m \sup a *r].
 intros.
-apply nat_case (mod n m). *)
+apply nat_case (n \mod m). *)