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