completed use of \mod and / notation

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

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index f9f0289a0bee7e2f7d9db983d021aec87e43d112..fc51b32ff4bce5c108565f56ddda782c7e6ecece 100644 (file)
--- 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)).