proposition: Lemma p_gcd_duv_rec : forall a b r : positive, (Zpos a mod Zpos b)%Z = Zpos r -> p_gcd_duv a b = (let (d, uv) := p_gcd_duv b r in let (u, v) := uv in (d, (v, (u - Zpos a / Zpos b * v)%Z))).
proof: Proof. intros a b r Hr. unfold p_gcd_duv. fold (p_gcd_duv b r). rewrite Fix_eq; simpl. case (rem_dec a b). rewrite Hr; intros; discriminate. intro Hex; elim Hex; intros r' Hr'. fold (p_gcd_duv b r'). rewrite Hr in Hr'. inversion Hr'. auto. apply pp_gcd_ind_ext. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)