proposition: Lemma fractran_step_contradict_reversible a b c d l : is_gcd b a 1 -> ~ divides b d -> exists (s t u : nat), (a,b) :: (c,d) :: l /F/ s ≻ u /\ (a,b) :: (c,d) :: l /F/ t ≻ u /\ s <> t.
proof: Proof. intros Hba Hbd. exists (c*b), (a*d), (a*c). constructor; [constructor; lia|]. constructor. - apply in_fractran_1. + intros Hb. now do 2 apply (is_rel_prime_div _ Hba) in Hb. + constructor. lia. - intros E. apply Hbd. apply (is_rel_prime_div _ Hba). now exists c. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)