proposition: Lemma Zrem_divides : forall a b, Z.rem a b = 0 <-> exists c, a = b*c.
proof: Proof. intros. zero_or_not b. - firstorder. - rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; subst; auto with zarith. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms