proposition: Lemma fractran_reversible_shorten {a b c d P s t} : fractran_reversible ((S a, b) :: (S c, d) :: P) -> ((S a, b) :: P /F/ s ≻ t) <-> ((S a, b) :: (S c, d) :: P /F/ s ≻ t).
proof: Proof. intros HP. assert (Hba : b <> 0 \/ S a <> 0) by lia. destruct (rel_prime_intro Hba) as [b' [a' [gab [H'b [H'a Hb'a']]]]]. rewrite H'b, H'a in *. assert (Hdc : d <> 0 \/ S c <> 0) by lia. destruct (rel_prime_intro Hdc) as [d' [c' [gcd [H'd [H'c Hd'c']]]]]. rewrite H'd, H'c in *. assert (Hgab : gab <> 0) by lia. assert (Hgcd : gcd <> 0) by lia. split. + intros [?|[Hb ?]]%fractran_step_cons_inv. * now apply in_fractran_0. * apply in_fractran_1; [easy|]. apply in_fractran_1; [|easy]. intros [m Hm]. apply Hb. eapply (fractran_reversible_shadow Hgab Hgcd HP Hb'a' Hd'c'). eassumption. + intros [?|[Hb H']]%fractran_step_cons_inv. * now apply in_fractran_0. * revert H'. intros [H'|[Hd ?]]%fractran_step_cons_inv. ** exfalso. apply Hb. eapply (fractran_reversible_shadow Hgab Hgcd HP Hb'a' Hd'c' s t). lia. ** now apply in_fractran_1. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)