+(*cut (n = r * p + (m / p * p + m \mod p)).*)
+(*lapply (div_mod m p H).
+rewrite > sym_times.
+rewrite > distr_times_plus.
+(*rewrite > (sym_times p (m/p)).*)
+(*rewrite > sym_times.*)
+rewrite > assoc_plus.
+autobatch paramodulation.
+rewrite < div_mod.
+assumption.
+assumption.
+*)