proposition: Lemma fractran_step_inv P x y : P /F/ x ≻ y -> exists l p q r, P = l++(p,q)::r /\ (forall u v, In (u,v) l -> ~ divides v (u*x)) /\ q*y=p*x.
proof: Proof. induction 1 as [ p q P x y H | u v P x y H1 H2 IH2 ]. + exists nil, p, q, P; simpl; tauto. + destruct IH2 as (l & p & q & r & -> & H4 & H5). exists ((u,v)::l), p, q, r; simpl; msplit 2; auto. intros ? ? [ H | H ]; auto; inversion H; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)