proposition: Lemma pp_gcd_ind_ext : forall (x : pp) (f g : forall y : pp, pp_lt y x -> positive * (Z * Z)), (forall (y : pp) (p : pp_lt y x), f y p = g y p) -> pp_gcd_ind x f = pp_gcd_ind x g.
proof: Proof. intros x; elim x; intros a b. intros f g Hext. simpl in |- *. case (rem_dec a b). auto. intro Hex; elim Hex; intros r Hr. rewrite Hext. auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)