proposition: Fact fractran_zero_num l x : Exists (fun c => fst c = 0) l -> exists y, l /F/ x ≻ y.
proof: Proof. induction 1 as [ (p,q) l | (p,q) l Hl IHl ]; simpl in *. + exists 0; constructor 1; subst; ring. + destruct (divides_dec (p*x) q) as [ (y & Hy) | H ]. * exists y; constructor 1; rewrite Hy; ring. * destruct IHl 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)