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