proposition: Lemma divide_eqm : forall x m, m <> 0 -> (x ≡ 0 [m] <-> (m | x)).
proof: Proof. intros x m Nm; split; rewrite mod0_eqm; intros H. apply Zmod_divide; auto. apply Zdivide_mod; auto. Qed.
imports: ZArith Znumtheory MyNat Ztools