proposition: Theorem verif_divide : forall m p:nat, 0 < m -> 0 < p -> (exists q:nat, m = q*p) -> (Z_of_nat m mod Z_of_nat p = 0)%Z.
proof: Proof. intros m p Hltm Hltp (q, Heq); rewrite Heq. rewrite inj_mult. replace (Z_of_nat q * Z_of_nat p)%Z with (0 + Z_of_nat q * Z_of_nat p)%Z; try ring. rewrite Z_mod_plus; auto. lia. Qed.
imports: ZArith Arith Lia