rewrite > distr_times_minus.
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
- elim H1.rewrite > H6.
- (* applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
+ elim H1.
+ (*
+ rewrite > H6.
+ applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
reflexivity. *);
- applyS (witness n ? ? (refl_eq ? ?)) timeout=50.
+ applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
(*
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.