proposition: Fact in_out_interval_dec i x : { in_interval i x } + { out_interval i x }.
proof: Proof. destruct i as (a,b); simpl. destruct (le_lt_dec a x); destruct (le_lt_dec b x); try (left; lia);right; lia. Qed.
imports: List Arith Nat Lia