proposition: Fact Z_coprime u v : (exists a b, a * Z.of_nat u + b*Z.of_nat v = 1) -> is_gcd u v 1%nat.
proof: Proof. intros (a & b & H). destruct (Z_pos_or_neg a) as [ Ha | Ha ]; destruct (Z_pos_or_neg b) as [ Hb | Hb ]. + apply bezout_sc with (a:= Z.to_nat a) (b := Z.to_nat b) (m := 0%nat). 2: left; apply divides_0. apply Nat2Z.inj. rewrite Nat2Z.inj_add. repeat rewrite Nat2Z.inj_mul. repeat rewrite Z2Nat.id; auto. + apply bezout_sc with (a:= Z.to_nat a) (b := 0%nat) (m := (Z.to_nat (-b)*v)%nat). 2: right; apply divides_mult, divides_refl. apply Nat2Z.inj. repeat rewrite Nat2Z.inj_add. repeat rewrite Nat2Z.inj_mul. repeat rewrite Z2Nat.id; auto; lia. + apply bezout_sc with (b:= Z.to_nat b) (a := 0%nat) (m := (Z.to_nat (-a)*u)%nat). 2: left; apply divides_mult, divides_refl. apply Nat2Z.inj. repeat rewrite Nat2Z.inj_add. repeat rewrite Nat2Z.inj_mul. repeat rewrite Z2Nat.id; auto; lia. + apply Z.lt_le_incl in Ha. apply Z.lt_le_incl in Hb. exfalso; revert H. generalize (Z.mul_nonpos_nonneg _ _ Ha (Nat2Z.is_nonneg u)). generalize (Z.mul_nonpos_nonneg _ _ Hb (Nat2Z.is_nonneg v)). intros; lia. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)