fact: Definition pp_gcd_ind (ab : pp) : (forall cd : pp, pp_lt cd ab -> positive * (Z * Z)) -> positive * (Z * Z) := prod_rec (fun ab : positive * positive => (forall cd : pp, pp_lt cd ab -> positive * (Z * Z)) -> positive * (Z * Z)) (fun (a b : positive) (Hind : forall cd : pp, pp_lt cd (a, b) -> positive * (Z * Z)) => match rem_dec a b with | inl _ => (b, (0%Z, 1%Z)) | inr (existT _ r' Hr') => let (d, uv) := Hind (b, r') (rem_lt a b r' Hr') in let (u, v) := uv in (d, (v, (u - Zpos a / Zpos b * v)%Z)) end) ab.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)