rewrite < H4.
apply sym_eq.
apply plus_to_minus.
-rewrite > div_mod m n in \vdash (? ? %).
rewrite > sym_times.
-apply eq_plus_to_le ? ? (m \mod n).
-reflexivity.
+apply div_mod.
assumption.
-rewrite > sym_times.
-apply div_mod.assumption.
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to