proposition: Fact fractran_zero_num_step l : Exists (fun c => fst c = 0) l -> forall x, exists y, l /F/ x ≻ y.
proof: Proof. induction 1 as [ (p,q) l Hl | (p,q) l Hl IHl ]; simpl in Hl. + intros x; exists 0; subst; constructor; lia. + intros x. destruct (divides_dec (p*x) q) as [ (y & Hy) | C ]. * exists y; constructor; rewrite Hy, Nat.mul_comm; auto. * destruct (IHl x) as (y & Hy); exists y; constructor 2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)