- |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);