proposition: Lemma in_itv x i : x \in i = let: Interval l u := i in match l with | BSide b lb => lb < x ?<= if b | BInfty b => b end && match u with | BSide b ub => x < ub ?<= if ~~ b | BInfty b => ~~ b end.
proof: Proof. by case: i => [[? ?|[]][|[]]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)