proposition: Corollary no_common_prime_is_coprime x y : x <> 0 -> (forall p, prime p -> p <d x -> p <d y -> False) -> is_gcd x y 1.
proof: Proof. intros Hx H; split; [ | split ]. + apply divides_1. + apply divides_1. + intros k H1 H2. destruct k as [ | [ | k ] ]. * apply divides_0_inv in H1; lia. * apply divides_1. * destruct prime_factor with (n := S (S k)) as (p & P1 & P2); try lia. exfalso; apply H with p; auto; apply divides_trans with (S (S k)); auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)