inductive divides (n,m:nat) : Prop \def
witness : \forall p:nat.m = times n p \to divides n m.
inductive divides (n,m:nat) : Prop \def
witness : \forall p:nat.m = times n p \to divides n m.
\forall n,m. O < n \to n \divides m \to (m \mod n) = O.
intros.
apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O)
\forall n,m. O < n \to n \divides m \to (m \mod n) = O.
intros.
apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O)