proposition: Lemma fractran_step_fun l x y1 y2 : fractran_regular l -> l /F/ x ≻ y1 -> l /F/ x ≻ y2 -> y1 = y2.
proof: Proof. intros H1 H2 ; revert H2 H1 y2. induction 1 as [ p q l x y1 H1 | p q l x y1 H1 H2 IH2 ]; intros H0 y2 H3; rewrite fractran_step_cons_inv in H3; destruct H3 as [ H3 | (H3 & H4) ]. + apply Forall_cons_inv, proj1 in H0. simpl in H0. revert H1; rewrite <- H3. apply mul_pos_inj_l; auto. + destruct H3; exists y1; rewrite <- H1; ring. + destruct H1; exists y2; rewrite <- H3; ring. + apply Forall_cons_inv, proj2 in H0; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)