proposition: Lemma Zmod_opp_zero : forall m a : Z, (m > 0)%Z -> (a mod m)%Z = 0%Z -> (- a mod m)%Z = 0%Z.
proof: Proof. intros m a Hm Ha. rewrite (Zmod_opp_elim m a Hm). rewrite Ha. unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r. apply (Z_mod_same m Hm). Qed.
imports: CoRN.model.Zmod.ZGcd