\lambda n,m,q,r:nat.r < m \land n=q*m+r).
*)
-theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to \lnot m=O.
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
intros 4.simplify.intros.elim H.absurd le (S r) O.
rewrite < H1.assumption.
exact not_le_Sn_O r.