proposition: Lemma p_gcd_rec_coeff_a : forall a b r : positive, (Zpos a mod Zpos b)%Z = Zpos r -> p_gcd_coeff_a a b = p_gcd_coeff_b b r.
proof: Proof. intros a b r Hr. unfold p_gcd_coeff_a in |- *. unfold p_gcd_coeff_b in |- *. rewrite (p_gcd_duv_rec a b r Hr). elim (p_gcd_duv b r); intros d uv; elim uv; intros u v. reflexivity. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)