proposition: Lemma Zgcd_coeff_b_zero_rht : forall a : Z, Zgcd_coeff_b a 0 = 0%Z.
proof: Proof. intro a. unfold Zgcd_coeff_b in |- *. rewrite Zgcd_duv_zero_rht. reflexivity. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)