proposition: Lemma p_gcd_lin_comb : forall a b : positive, Zpos (p_gcd a b) = (p_gcd_coeff_a a b * Zpos a + p_gcd_coeff_b a b * Zpos b)%Z.
proof: Proof. intros a b. apply (pp_gcd_lin_comb (a, b)). Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)