proposition: Lemma Zgcd_lin_comb : forall a b : Z, Zgcd a b = (Zgcd_coeff_a a b * a + Zgcd_coeff_b a b * b)%Z.
proof: Proof. intros a b. unfold Zgcd, Zgcd_coeff_a, Zgcd_coeff_b in |- *. case a; case b; simpl in |- *; intros; repeat rewrite Zmult_opp_comm; simpl in |- *; try rewrite p_gcd_lin_comb; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)