include "datatypes/constructors.ma".
include "nat/exp.ma".
include "nat/gcd.ma".
-include "nat/relevant_equations.ma". (* required by auto paramod *)
+include "nat/relevant_equations.ma". (* required by autobatch paramod *)
let rec p_ord_aux p n m \def
match n \mod m with
apply (absurd ? ? H10 H7).
(* rewrite > H6.
rewrite > H8. *)
-auto paramodulation.
+autobatch paramodulation.
unfold prime in H. elim H. assumption.
qed.
apply (lt_to_not_eq O ? H).
rewrite > H7.
rewrite < H10.
- auto
+ autobatch
]
|elim c
[rewrite > sym_gcd.
|apply lt_O_exp.apply lt_to_le.assumption
|rewrite > sym_gcd.
(* hint non trova prime_to_gcd_SO e
- auto non chiude il goal *)
+ autobatch non chiude il goal *)
apply prime_to_gcd_SO
[assumption|assumption]
|assumption
|apply lt_O_exp.apply lt_to_le.assumption
|rewrite > sym_gcd.
(* hint non trova prime_to_gcd_SO e
- auto non chiude il goal *)
+ autobatch non chiude il goal *)
apply prime_to_gcd_SO
[assumption|assumption]
|rewrite > sym_gcd. assumption