(*rewrite > (assoc_times (n/p) p (m \mod p)).
rewrite > (sym_times p (m \mod p)).
rewrite < (assoc_times (n/p) (m \mod p) p).
(*rewrite > (assoc_times (n/p) p (m \mod p)).
rewrite > (sym_times p (m \mod p)).
rewrite < (assoc_times (n/p) (m \mod p) p).