proposition: Lemma mul_itv_boundr_subproof b1 b2 (x1 x2 : R) : (BLeft 0%R <= BLeft x1 -> BLeft 0%R <= BLeft x2 -> 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: b1 b2 => [b1b b1 | []] [b2b b2 | []] //=; last first. - move: b2 b2b => [[|p2]|p2] [] // _ + _ +; rewrite !bnd_simp => le1 le2. + by move: (le_lt_trans le1 le2); rewrite ltxx. + by move: (conj le1 le2) => /andP/le_anti <-; rewrite mulr0. - move: b1 b1b => [[|p1]|p1] [] // + _ + _; rewrite !bnd_simp => le1 le2. + by move: (le_lt_trans le1 le2); rewrite ltxx. + by move: (conj le1 le2) => /andP/le_anti <-; rewrite mul0r. case: b1 => [[|p1]|p1]. - case: b1b. by rewrite !bnd_simp => l _ l' _; move: (le_lt_trans l l'); rewrite ltxx. by move: b2b b2 => [] [[|p2]|p2]; rewrite !bnd_simp; first (by move=> _ l _ l'; move: (le_lt_trans l l'); rewrite ltxx); move=> l _ l' _; move: (conj l l') => /andP/le_anti <-; rewrite mul0r. - rewrite if_same. case: b2 => [[|p2]|p2]. + case: b2b => _ + _ +; rewrite !bnd_simp => l l'. by move: (le_lt_trans l l'); rewrite ltxx. by move: (conj l l') => /andP/le_anti <-; rewrite mulr0. + move: b1b b2b => [] []; rewrite !bnd_simp; rewrite -[intRing.mulz ?[a] ?[b]]/((Posz ?[a]) * ?[b])%R intrM. * exact: ltr_pM. * move=> x1ge0 x2ge0 ltx1p1 lex2p2. have: x1 * p2.+1%:~R < p1.+1%:~R * p2.+1%:~R. by rewrite ltr_pM2r // ltr0z. exact/le_lt_trans/ler_pM. * move=> x1ge0 x2ge0 lex1p1 ltx2p2. have: p1.+1%:~R * x2 < p1.+1%:~R * p2.+1%:~R. by rewrite ltr_pM2l // ltr0z. exact/le_lt_trans/ler_pM. * exact: ler_pM. + case: b2b => _ + _; rewrite 2!bnd_simp => l l'. by move: (le_lt_trans l l'); rewrite ltr0z. by move: (le_trans l l'); rewrite ler0z. - case: b1b => + _ + _; rewrite 2!bnd_simp => l l'. by move: (le_lt_trans l l'); rewrite ltr0z. by move: (le_trans l l'); rewrite ler0z. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed