fact: Definition bound_meet bl br : itv_bound T := match bl, br with | -oo, _ | _, -oo => -oo | +oo, b | b, +oo => b | BSide xb x, BSide yb y => BSide (((x <= y) && xb) || ((y <= x) && yb)) (x `&` y) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)