proposition: Lemma Zgcd_coeff_a_Zopp_l : forall a b : Z, Zgcd_coeff_a (- a) b = (- Zgcd_coeff_a a b)%Z.
proof: Proof. intros. unfold Zgcd_coeff_a in |- *. rewrite Zgcd_duv_Zopp_l. elim (Zgcd_duv a b); intros d uv; elim uv; intros u v. reflexivity. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)