proposition: Lemma Zmodeq_zero : forall a : Z, Zmodeq a 0 <-> Zdivides m a.
proof: Proof. unfold Zmodeq in |- *; unfold Zdivides in |- *. intros. unfold Zminus in |- *. simpl in |- *. rewrite Zplus_0_r. tauto. Qed.
imports: CoRN.model.Zmod.ZGcd