intros 2.elim m.elim (not_le_Sn_O O H).
simplify.
apply div_aux_mod_aux.
qed.
inductive div_mod_spec (n,m,q,r:nat) : Prop \def
intros 2.elim m.elim (not_le_Sn_O O H).
simplify.
apply div_aux_mod_aux.
qed.
inductive div_mod_spec (n,m,q,r:nat) : Prop \def