proposition: Lemma Zmodeq_opp_intro : forall a b : Z, Zmodeq (- a) (- b) -> Zmodeq a b.
proof: Proof. intros a b H. rewrite <- (Z.opp_involutive a). rewrite <- (Z.opp_involutive b). apply (Zmodeq_opp_elim _ _ H). Qed.
imports: CoRN.model.Zmod.ZGcd