rewrite < sym_times.rewrite > assoc_times.
rewrite < (assoc_times q).
rewrite < (sym_times n).
rewrite < distr_times_minus.
apply (witness ? ? (n1*a1-q*a)).reflexivity
rewrite < sym_times.rewrite > assoc_times.
rewrite < (assoc_times q).
rewrite < (sym_times n).
rewrite < distr_times_minus.
apply (witness ? ? (n1*a1-q*a)).reflexivity