proposition: Lemma opp_itv_ge0_subproof b : (BLeft 0%R <= opp_itv_bound_subdef b)%O = (b <= BRight 0%R)%O.
proof: Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp oppr_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed