proposition: Lemma Zmodeq_opp_elim : forall a b : Z, Zmodeq a b -> Zmodeq (- a) (- b).
proof: Proof. intros a b H. replace (- a)%Z with (-1 * a)%Z; auto with zarith. replace (- b)%Z with (-1 * b)%Z; auto with zarith. apply Zmodeq_mult_elim. apply Zmodeq_refl. exact H. Qed.
imports: CoRN.model.Zmod.ZGcd