applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
|(* second case *)
rewrite > (times_n_SO p).rewrite < H6.
rewrite > distr_times_minus.
rewrite > (sym_times p (a1*m)).
rewrite > (assoc_times a1).
applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
|(* second case *)
rewrite > (times_n_SO p).rewrite < H6.
rewrite > distr_times_minus.
rewrite > (sym_times p (a1*m)).
rewrite > (assoc_times a1).