proposition: Lemma opp_itv_boundr_subproof (x : R) b : (BRight (- x)%R <= Itv.map_itv_bound intr (opp_itv_bound_subdef b))%O = (Itv.map_itv_bound intr b <= BLeft x)%O.
proof: Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz ?lerN2 // ltrN2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed