proposition: Lemma fractran_reversible_shadow {a b c d P x y} : x <> 0 -> y <> 0 -> fractran_reversible ((a * x, b * x) :: (c * y, d * y) :: P) -> is_gcd b a 1 -> is_gcd d c 1 -> forall s t, (c * y) * s = t * (d * y) -> exists u, (a * x) * s = u * (b * x).
proof: Proof. intros ?? HP Hba Hdc. destruct (divides_dec d b) as [[u Hu]|Hb]. - subst d. intros s t Hst. assert (Hubcs : divides (u * b) (c * s)) by (exists t; nia). destruct (is_rel_prime_div s Hdc Hubcs) as [k ?]. subst s. exists (a*k*u). nia. - exfalso. destruct (fractran_step_contradict_reversible a b c d P Hba Hb) as [s [t [u [? [? Hst]]]]]. apply Hst. enough (H_extend : forall s' t', (a, b) :: (c, d) :: P /F/ s' ≻ t' -> (a * x, b * x) :: (c * y, d * y) :: P /F/ s' ≻ t'). { apply (HP s t u); now apply H_extend. } intros s' t' [|[H'b Hs't']]%fractran_step_cons_inv. + apply in_fractran_0. nia. + revert Hs't'. intros [|[H'd Hs't']]%fractran_step_cons_inv. * apply in_fractran_1. { intros [k ?]. apply H'b. exists k. nia. } apply in_fractran_0. nia. * apply in_fractran_1. { intros [k1 ?]. apply H'b. exists k1. nia. } apply in_fractran_1. { intros [k2 ?]. apply H'd. exists k2. nia. } exact Hs't'. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)