[ 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.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.