[ apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| apply lt_SO_smallest_factor; assumption; ]
- | letin x \def le.autobatch.
- (*
- apply divides_smallest_factor_n;
- apply (trans_lt ? (S O));
- [ unfold lt; apply le_n;
- | assumption; ] *) ] ]
- | autobatch.
+ | apply divides_smallest_factor_n;
+ autobatch; ] ]
+ | apply prime_to_nth_prime;
+ autobatch.
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
assumption.unfold Not.
intro.
cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
- [unfold Not in Hcut1.autobatch.
+ [ apply Hcut1; autobatch depth=2;
(*
apply Hcut1.apply divides_to_mod_O;
[ apply lt_O_nth_prime_n.
| assumption.
]
*)
- |letin z \def le.
- cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
- [2: rewrite < H1.assumption.|letin x \def le.autobatch width = 4 depth = 2]
- (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
- ].
-(*
- apply (p_ord_aux_to_not_mod_O n n ? q r);
+ | unfold p_ord in H2; lapply depth=0 le_n; autobatch width = 4 depth = 2;
+ (*apply (p_ord_aux_to_not_mod_O n n ? q r);
[ apply lt_SO_nth_prime_n.
| assumption.
| apply le_n.
| rewrite < H1.assumption.
- ]
+ ]*)
].
-*)
+
apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
apply divides_to_max_prime_factor.
assumption.assumption.