rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.
rewrite < (assoc_times a1).rewrite < (sym_times n).
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.
rewrite < (assoc_times a1).rewrite < (sym_times n).