apply div_mod_spec_div_mod.assumption.
constructor 1.assumption.
rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
qed.
apply div_mod_spec_div_mod.assumption.
constructor 1.assumption.
rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
qed.