+lemma div_plus_times: \forall m,q,r:nat. r < m \to (q*m+r)/ m = q.
+intros.
+apply (div_mod_spec_to_eq (q*m+r) m ? ((q*m+r) \mod m) ? r)
+ [apply div_mod_spec_div_mod.
+ apply (le_to_lt_to_lt ? r)
+ [apply le_O_n|assumption]
+ |apply div_mod_spec_intro[assumption|reflexivity]
+ ]
+qed.
+
+lemma mod_plus_times: \forall m,q,r:nat. r < m \to (q*m+r) \mod m = r.
+intros.
+apply (div_mod_spec_to_eq2 (q*m+r) m ((q*m+r)/ m) ((q*m+r) \mod m) q r)
+ [apply div_mod_spec_div_mod.
+ apply (le_to_lt_to_lt ? r)
+ [apply le_O_n|assumption]
+ |apply div_mod_spec_intro[assumption|reflexivity]
+ ]
+qed.
+