proposition: Lemma gcd_opp_r : forall (d : nat) (x y : Z), gcd x y d -> gcd x (- y) d.
proof: Proof. unfold gcd in |- *. unfold common_div in |- *. intros. elim H. intros. elim H0. intros. split. split. assumption. rewrite <- abs_opp. assumption. intros. elim H4. intros. apply H1. split. assumption. rewrite abs_opp. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo