fact: Definition le_bound b1 b2 := match b1, b2 with | -oo, _ | _, +oo => true | BSide b1 x1, BSide b2 x2 => x1 < x2 ?<= if b2 ==> b1 | _, _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)