proposition: Lemma mul_itv_boundr'_subproof b1 b2 (x1 x2 : R) : (BLeft 0%:R <= BLeft x1 -> BRight 0%:Z <= b2 -> BRight x1 <= Itv.map_itv_bound intr b1 -> BRight x2 <= Itv.map_itv_bound intr b2 -> BRight (x1 * x2) <= Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O.
proof: Proof. move=> x1ge0 b2ge0 lex1b1 lex2b2. have [x2ge0 | x2lt0] := leP 0 x2; first exact: mul_itv_boundr_subproof. have lem0 : (BRight (x1 * x2) <= BRight 0%R)%O. by rewrite bnd_simp mulr_ge0_le0 // ltW. apply: le_trans lem0 _. move: b1 b2 lex1b1 lex2b2 b2ge0 => [b1b b1 | []] [b2b b2 | []] //=; last first. - by move: b2 b2b => [[|?]|?] []. - move: b1 b1b => [[|p1]|p1] [] //. by rewrite leBRight_ltBLeft => /(le_lt_trans x1ge0); rewrite ltxx. case: b1 => [[|p1]|p1]. - case: b1b; last by move: b2b b2 => [] [[|]|]. by rewrite leBRight_ltBLeft => /(le_lt_trans x1ge0); rewrite ltxx. - rewrite if_same. case: b2 => [[|p2]|p2]; first (by case: b2b); last by case: b2b. by rewrite if_same => _ _ _ /=; rewrite leBSide ltrW_lteif // ltr0z. - rewrite leBRight_ltBLeft => /(le_lt_trans x1ge0). by case: b1b; rewrite bnd_simp ?ltr0z // ler0z. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed