proposition: Lemma Zgcd_coeff_a_divisor : forall a b : Z, a <> 0%Z -> Zdivides b a -> Zgcd_coeff_a a b = 0%Z.
proof: Proof. intros. unfold Zgcd_coeff_a in |- *. rewrite Zgcd_duv_divisor; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)