More notation here and there: \sup, \divides, \ndivides, !

[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 43b942a5b828ea0305d7d3442e9f1db824c3ca8e..1b946be522c143b6be9e1082dab079c9b82a86dd 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -25,7 +25,7 @@ definition max_prime_factor \def \lambda n:nat.
 
 (* max_prime_factor is indeed a factor *)
 theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to
-divides (nth_prime (max_prime_factor n)) n.
+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.
@@ -48,7 +48,7 @@ apply prime_to_nth_prime.
 apply prime_smallest_factor_n.assumption.
 qed.
 
-theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to divides n m \to 
+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
@@ -60,7 +60,7 @@ change with divides_b (nth_prime (max_prime_factor n)) m = true.
 apply divides_to_divides_b_true.
 cut prime (nth_prime (max_prime_factor n)).
 apply lt_O_nth_prime_n.apply prime_nth_prime.
-cut divides (nth_prime (max_prime_factor n)) n.
+cut nth_prime (max_prime_factor n) \divides n.
 apply transitive_divides ? n.
 apply divides_max_prime_factor_n.
 assumption.assumption.
@@ -81,13 +81,13 @@ rewrite > H1.
 cut max_prime_factor r \lt max_prime_factor n \lor
     max_prime_factor r = max_prime_factor n.
 elim Hcut.assumption.
-absurd (divides (nth_prime (max_prime_factor n)) r).
+absurd nth_prime (max_prime_factor n) \divides r.
 rewrite < H4.
 apply divides_max_prime_factor_n.
 assumption.
-change with (divides (nth_prime (max_prime_factor n)) r) \to False.
+change with nth_prime (max_prime_factor n) \divides r \to False.
 intro.
-cut \not (mod r (nth_prime (max_prime_factor n))) = O.
+cut \lnot (mod r (nth_prime (max_prime_factor n))) = O.
 apply Hcut1.apply divides_to_mod_O.
 apply lt_O_nth_prime_n.assumption.
 apply plog_aux_to_not_mod_O n n ? q r.
@@ -266,12 +266,12 @@ assumption.
 apply sym_eq. apply S_pred.
 cut O < q \lor O = q.
 elim Hcut2.assumption.
-absurd divides (nth_prime p) (S (S m1)).
+absurd nth_prime p \divides S (S m1).
 apply divides_max_prime_factor_n (S (S m1)).
 simplify.apply le_S_S.apply le_S_S. apply le_O_n.
 cut (S(S m1)) = r.
 rewrite > Hcut3 in \vdash (? (? ? %)).
-change with divides (nth_prime p) r \to False.
+change with nth_prime p \divides r \to False.
 intro.
 apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.
 apply lt_SO_nth_prime_n.
@@ -332,13 +332,13 @@ match f with
 | (nf_cons n g) \Rightarrow max_p_exponent g].
 
 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat. 
-divides (nth_prime ((max_p f)+i)) (defactorize_aux f i).
+nth_prime ((max_p f)+i) \divides defactorize_aux f i.
 intro.
 elim f.simplify.apply witness ? ? ((nth_prime i) \sup n).
 reflexivity.
 change with 
-divides (nth_prime (S(max_p n1)+i)) 
-((nth_prime i) \sup n *(defactorize_aux n1 (S i))).
+nth_prime (S(max_p n1)+i) \divides
+(nth_prime i) \sup n *(defactorize_aux n1 (S i)).
 elim H (S i).
 rewrite > H1.
 rewrite < sym_times.
@@ -350,11 +350,11 @@ qed.
 
 theorem divides_exp_to_divides: 
 \forall p,n,m:nat. prime p \to 
-divides p (n \sup m) \to divides p n.
+p \divides n \sup m \to p \divides n.
 intros 3.elim m.simplify in H1.
 apply transitive_divides p (S O).assumption.
 apply divides_SO_n.
-cut divides p n \lor divides p (n \sup n1).
+cut p \divides n \lor p \divides n \sup n1.
 elim Hcut.assumption.
 apply H.assumption.assumption.
 apply divides_times_to_divides.assumption.
@@ -363,7 +363,7 @@ qed.
 
 theorem divides_exp_to_eq: 
 \forall p,q,m:nat. prime p \to prime q \to
-divides p (q \sup m) \to p = q.
+p \divides q \sup m \to p = q.
 intros.
 simplify in H1.
 elim H1.apply H4.
@@ -373,10 +373,10 @@ simplify in H.elim H.assumption.
 qed.
 
 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
-i < j \to \not divides (nth_prime i) (defactorize_aux f j).
+i < j \to nth_prime i \ndivides defactorize_aux f j.
 intro.elim f.
 change with
-divides (nth_prime i) ((nth_prime j) \sup (S n)) \to False.
+nth_prime i \divides (nth_prime j) \sup (S n) \to False.
 intro.absurd (nth_prime i) = (nth_prime j).
 apply divides_exp_to_eq ? ? (S n).
 apply prime_nth_prime.apply prime_nth_prime.
@@ -386,10 +386,10 @@ intro.cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H2.
 change with 
-divides (nth_prime i) ((nth_prime j) \sup n *(defactorize_aux n1 (S j))) \to False.
+nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False.
 intro.
-cut divides (nth_prime i) ((nth_prime j) \sup n)
-\lor divides (nth_prime i) (defactorize_aux n1 (S j)).
+cut nth_prime i \divides (nth_prime j) \sup n
+\lor nth_prime i \divides defactorize_aux n1 (S j).
 elim Hcut.
 absurd (nth_prime i) = (nth_prime j).
 apply divides_exp_to_eq ? ? n.
@@ -420,11 +420,11 @@ assumption.
 absurd defactorize_aux (nf_last n) i =
 defactorize_aux (nf_cons n1 n2) i.
 rewrite > H2.reflexivity.
-absurd divides (nth_prime (S(max_p n2)+i)) (defactorize_aux (nf_cons n1 n2) i).
+absurd nth_prime (S(max_p n2)+i) \divides defactorize_aux (nf_cons n1 n2) i.
 apply divides_max_p_defactorize.
 rewrite < H2.
 change with 
-(divides (nth_prime (S(max_p n2)+i)) ((nth_prime i) \sup (S n))) \to False.
+(nth_prime (S(max_p n2)+i) \divides (nth_prime i) \sup (S n)) \to False.
 intro.
 absurd nth_prime (S (max_p n2) + i) = nth_prime i.
 apply divides_exp_to_eq ? ? (S n).
@@ -441,11 +441,11 @@ elim g.
 absurd defactorize_aux (nf_last n2) i =
 defactorize_aux (nf_cons n n1) i.
 apply sym_eq. assumption.
-absurd divides (nth_prime (S(max_p n1)+i)) (defactorize_aux (nf_cons n n1) i).
+absurd nth_prime (S(max_p n1)+i) \divides defactorize_aux (nf_cons n n1) i.
 apply divides_max_p_defactorize.
 rewrite > H2.
 change with 
-(divides (nth_prime (S(max_p n1)+i)) ((nth_prime i) \sup (S n2))) \to False.
+(nth_prime (S(max_p n1)+i) \divides (nth_prime i) \sup (S n2)) \to False.
 intro.
 absurd nth_prime (S (max_p n1) + i) = nth_prime i.
 apply divides_exp_to_eq ? ? (S n2).