fact: Definition itv_rewrite i x : Type := let: Interval l u := i in (match l with | BLeft a => (a <= x) * (x < a = false) | BRight a => (a <= x) * (a < x) * (x <= a = false) * (x < a = false) | -oo => forall x : T, x == x | +oo => forall b : bool, unkeyed b = false end * match u with | BRight b => (x <= b) * (b < x = false) | BLeft b => (x <= b) * (x < b) * (b <= x = false) * (b < x = false) | +oo => forall x : T, x == x | -oo => forall b : bool, unkeyed b = false end * match l, u with | BLeft a, BRight b => (a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b]) | BLeft a, BLeft b => (a <= b) * (a < b) * (b <= a = false) * (b < a = false) * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) | BRight a, BRight b => (a <= b) * (a < b) * (b <= a = false) * (b < a = false) * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) | BRight a, BLeft b => (a <= b) * (a < b) * (b <= a = false) * (b < a = false) * (a \in `[a, b]) * (a \in `[a, b[) * (b \in `[a, b]) * (b \in `]a, b]) | _, _ => forall x : T, x == x end)%type.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)