proposition: Lemma p_gcd_duv_rec_zero : forall a b : positive, (Zpos a mod Zpos b)%Z = 0%Z -> p_gcd_duv a b = (b, (0%Z, 1%Z)).
proof: Proof. intros a b Hr. unfold p_gcd_duv. rewrite Fix_eq. simpl. case (rem_dec a b). auto. intro Hex; elim Hex; intros r' Hr'. rewrite Hr in Hr'. discriminate. apply pp_gcd_ind_ext. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)