|right.
cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
[elim Hcut1.elim H3.elim H4
- [(* first case *)
- rewrite > (times_n_SO q).rewrite < H5.
+ [rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
- elim H1. autobatch;
- (*
+ elim H1.
+ autobatch by witness;
+ (*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
applyS (witness n ? ? (refl_eq ? ?)).
|(* second case *)
rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
- elim H1. autobatch;
+ elim H1. autobatch by witness;
(*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
|cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
[elim Hcut1.elim H4.elim H5
[(* first case *)
+ elim H2.
rewrite > (times_n_SO p).rewrite < H6.
rewrite > distr_times_minus.
- rewrite > (sym_times p (a1*m)).
- rewrite > (assoc_times a1).
- elim H2.rewrite > H7.
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
- |(* second case *)
+ autobatch by witness, divides_minus.
+ |(* second case *)
+ elim H2.
rewrite > (times_n_SO p).rewrite < H6.
rewrite > distr_times_minus.
- rewrite > (sym_times p (a1*m)).
- rewrite > (assoc_times a1).
- elim H2.rewrite > H7.
- applyS (witness n ? ? (refl_eq ? ?)).
+ autobatch by witness, divides_minus.
](* end second case *)
|rewrite < H1.apply eq_minus_gcd.
]
rewrite > H4 in H2.
elim (divides_times_to_divides ? ? ? H H2)
[apply False_ind.apply H1.assumption
- |elim H5.
+ |elim H5.
+ autobatch by transitive_divides, H5, reflexive_divides,divides_times.
+ (*
apply (witness ? ? n2).
rewrite > sym_times in ⊢ (? ? ? (? % ?)).
rewrite > assoc_times.
- rewrite < H6.assumption
+ autobatch.
+ (*rewrite < H6.assumption*)
+ *)
]
qed.
\ No newline at end of file