[ apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| apply lt_SO_smallest_factor; assumption; ]
- | letin x \def le.autobatch new.
+ | letin x \def le.autobatch.
(*
apply divides_smallest_factor_n;
apply (trans_lt ? (S O));
assumption; *) ]
qed.
+lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
+ \exists p.p \leq m \land prime p \land p \divides n.
+intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
+ [split
+ [apply divides_to_le
+ [apply lt_to_le;assumption
+ |apply divides_max_prime_factor_n;assumption]
+ |apply prime_nth_prime;]
+ |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
+ assumption]
+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.unfold max_prime_factor.
assumption.unfold Not.
intro.
cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
- [unfold Not in Hcut1.autobatch new.
+ [unfold Not in Hcut1.autobatch.
(*
apply Hcut1.apply divides_to_mod_O;
[ apply lt_O_nth_prime_n.