theorem div_times: \forall n,m:nat. div ((S n)*m) (S n) = m.
intros.
apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O.
+goal 15. (* ?11 is closed with the following tactics *)
apply div_mod_spec_div_mod.
simplify.apply le_S_S.apply le_O_n.
apply div_mod_spec_times.