proposition: Lemma bezout_inj : forall a b, {u : Z & {v | u * a + v * b = Z.gcd a b}}.
proof: Proof. intros a b. destruct (extgcd a b) as [[u v] d] eqn:Heqd. apply extgcd_correct in Heqd. destruct Heqd as [E Hgc]. pose proof (Zgcd_is_gcd a b) as H. rewrite <- Hgc in H; clear Hgc. destruct (Z_le_dec 0 d) as [L|L]. exists u; exists v. rewrite (Zis_gcd_gcd _ _ _ L H). auto. exists (- u); exists (- v). assert (L2 : 0 <= - d) by lia. rewrite (Zis_gcd_gcd _ _ _ L2). rewrite <- E; ring. apply Zis_gcd_opp, Zis_gcd_sym; auto. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm