(* 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.
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
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.
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.
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.
| (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.
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.
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.
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.
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.
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).
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).