proposition: Lemma Zgcd_duv_Zopp_r : forall a b : Z, Zgcd_duv a (- b) = (let (d, uv) := Zgcd_duv a b in let (u, v) := uv in (d, (u, (- v)%Z))).
proof: Proof. intros a b. case a; case b; intros; simpl in |- *; repeat rewrite Z.opp_involutive; reflexivity. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)