proposition: Lemma opp_itv_gt0_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 // oppr_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed