proposition: Lemma mul_itv_boundl_subproof b1 b2 (x1 x2 : R) : (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 -> Itv.map_itv_bound intr b1 <= BLeft x1 -> Itv.map_itv_bound intr b2 <= BLeft x2 -> Itv.map_itv_bound intr (mul_itv_boundl_subdef b1 b2) <= BLeft (x1 * x2))%O.
proof: Proof. move: b1 b2 => [[] b1 | []//] [[] b2 | []//] /=; rewrite 4!bnd_simp. - set bl := match b1 with 0%Z => _ | _ => _ end. have -> : bl = BLeft (b1 * b2). rewrite {}/bl; move: b1 b2 => [[|p1]|p1] [[|p2]|p2]; congr BLeft. by rewrite mulr0. rewrite -2!(ler0z R) bnd_simp intrM; exact: ler_pM. - case: b1 => [[|p1]|//]; rewrite -2!(ler0z R) !bnd_simp ?intrM. by move=> _ geb2 ? ?; apply: mulr_ge0 => //; apply/(le_trans geb2)/ltW. move=> p1gt0 b2ge0 lep1x1 ltb2x2. have: (Posz p1.+1)%:~R * x2 <= x1 * x2. by rewrite ler_pM2r //; apply: le_lt_trans ltb2x2. by apply: lt_le_trans; rewrite ltr_pM2l // ltr0z. - case: b2 => [[|p2]|//]; rewrite -2!(ler0z R) !bnd_simp ?intrM. by move=> geb1 _ ? ?; apply: mulr_ge0 => //; apply/(le_trans geb1)/ltW. move=> b1ge0 p2gt0 ltb1x1 lep2x2. have: b1%:~R * x2 < x1 * x2; last exact/le_lt_trans/ler_pM. by rewrite ltr_pM2r //; apply: lt_le_trans lep2x2; rewrite ltr0z. - rewrite -2!(ler0z R) bnd_simp intrM; exact: ltr_pM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed