proposition: Lemma rel_prime_intro {p q} : (p <> 0 \/ q <> 0) -> { a & { b & { g | p = a*g /\ q = b*g /\ is_gcd a b 1 } } }.
proof: Proof. intros ?. assert (Hg := gcd_spec p q). assert (gcd p q <> 0). { intros H'g. rewrite H'g in Hg. apply is_gcd_0 in Hg. tauto. } destruct (divides_dec p (gcd p q)) as [[a Ha]|]. 2: { unfold is_gcd in Hg. tauto. } destruct (divides_dec q (gcd p q)) as [[b Hb]|]. 2: { unfold is_gcd in Hg. tauto. } exists a, b, (gcd p q). split; [easy|split;[easy|]]. split; [apply divides_1|]. split; [apply divides_1|]. intros [|[|k]]. - intros [??] [??]. nia. - intros _ _. now exists 1. - intros [ka ?] [kb ?]. subst a b. exfalso. destruct Hg as [[??] [[??] Hpq]]. destruct (Hpq (S (S k) * (gcd p q))) as [k' ?]. + exists ka. nia. + exists kb. nia. + destruct k' as [|?]; nia. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)