proposition: Lemma Zgcd_coeff_b_rec : forall a b : Z, b <> 0%Z -> Zgcd_coeff_b a b = (Zgcd_coeff_a b (Z.abs a mod Z.abs b) - Z.sgn b * (Z.abs a / Z.abs b) * Zgcd_coeff_b b (Z.abs a mod Z.abs b))%Z.
proof: Proof. intros a b Hb. unfold Zgcd_coeff_a in |- *. unfold Zgcd_coeff_b in |- *. rewrite Zgcd_duv_rec. elim (Zgcd_duv b (Z.abs a mod Z.abs b)); intros d uv; elim uv; intros u v. reflexivity. exact Hb. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)