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.
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.