proposition: Lemma Zgcd_duv_rec : forall a b : Z, b <> 0%Z -> Zgcd_duv a b = (let (d, uv) := Zgcd_duv b (Z.abs a mod Z.abs b) in let (u, v) := uv in (d, ((Z.sgn a * v)%Z, (u - Z.sgn b * (Z.abs a / Z.abs b) * v)%Z))).
proof: Proof. intros a b Hb. set (B := b) in *. cut (B = b). case b. intro HB'. rewrite HB' in Hb. elim Hb. reflexivity. intros pb HB'. rewrite HB'. rewrite Zgcd_duv_rec_subcase. unfold Z.abs, Z.sgn in |- *. fold (Z.abs a) in |- *. fold (Z.sgn a) in |- *. elim (Zgcd_duv (Zpos pb) (Z.abs a mod Zpos pb)); intros d uv; elim uv; intros u v. rewrite Zmult_1_l. reflexivity. intros pb HB'. rewrite HB'. fold (- Zpos pb)%Z in |- *. rewrite Zgcd_duv_Zopp_r. rewrite Zgcd_duv_Zopp_l. rewrite Zgcd_duv_rec_subcase. unfold Z.opp, Z.abs, Z.sgn in |- *. fold (Z.abs a) in |- *. fold (Z.sgn a) in |- *. elim (Zgcd_duv (Zpos pb) (Z.abs a mod Zpos pb)); intros d uv; elim uv; intros u v. fold (- u)%Z in |- *. rewrite Zopp_mult_distr_l_reverse. unfold Zminus in |- *. rewrite <- Zopp_plus_distr. auto with zarith. auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)