proposition: Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) -> b = a * (b / a).
proof: Proof. intros Ha H. rewrite (Z.div_mod b a) at 1. + rewrite Zdivide_mod; auto with zarith. + auto using Z_lt_neq. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat