proposition: Lemma p_gcd_coeff_a_rec_zero : forall a b : positive, (Zpos a mod Zpos b)%Z = 0%Z -> p_gcd_coeff_a a b = 0%Z.
proof: Proof. intros a b H0. unfold p_gcd_coeff_a in |- *. rewrite p_gcd_duv_rec_zero. reflexivity. exact H0. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)