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