proposition: Lemma Zgcd_duv_abs : forall a b : Z, Zgcd_duv a b = (let (d, uv) := Zgcd_duv (Z.abs a) (Z.abs b) in let (u, v) := uv in (d, ((Z.sgn a * u)%Z, (Z.sgn b * v)%Z))).
proof: Proof. intros a b. case a; case b; intros; unfold Z.abs, Z.sgn, Zgcd_duv in |- *; repeat (fold (- (1))%Z in |- *; rewrite <- Zopp_mult_distr_l); repeat rewrite Zmult_1_l; reflexivity. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)