proposition: Lemma Zmod_divides : forall a b, b<>0 -> (a mod b = 0 <-> exists c, a = b*c).
proof: Proof. intros. rewrite Z.mod_divide; trivial. split; intros (c,Hc); exists c; subst; auto with zarith. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms