proposition: Lemma mul_inum_subproof (xi yi : interval int) (x : {itv R & xi}) (y : {itv R & yi}) (r := mul_itv_subdef xi yi) : Itv.spec r (x%:inum * y%:inum).
proof: Proof. rewrite {}/r. move: xi x yi y => [lx ux] [x /= /andP[+ +]] [ly uy] [y /= /andP[+ +]]. rewrite -/(interval_sign (Interval lx ux)). rewrite -/(interval_sign (Interval ly uy)). have empty10 (z : R) l u : (u <= l)%O -> (Itv.map_itv_bound [eta intr] l <= BLeft z)%O -> (BRight z <= Itv.map_itv_bound [eta intr] u)%O -> False. move=> leul; rewrite leBRight_ltBLeft => /le_lt_trans /[apply]. rewrite lt_def => /andP[/[swap]] => + /ltac:(apply/negP). rewrite negbK; move: leul => /(Itv.le_map_itv_bound R) le1 le2. by apply/eqP/le_anti; rewrite le1. pose opp := opp_itv_bound_subdef. pose mull := mul_itv_boundl_subdef. pose mulr := mul_itv_boundr_subdef. have [leuxlx|-> ->|lxneg uxneg|lxpos uxpos|lxneg uxpos] := interval_signP. - move=> + + /ltac:(exfalso); exact: empty10. - rewrite 2!bnd_simp => lex1 lex2 ley1 ley2. have -> : x = 0 by apply: le_anti; rewrite lex1 lex2. rewrite mul0r. case: interval_signP; [|by move=> _ _; rewrite /Itv.itv_cond in_itv/= lexx..]. by move=> leul; exfalso; move: ley1 ley2; apply: empty10. - move=> lelxx lexux. have xneg : x <= 0. move: (le_trans lexux (Itv.le_map_itv_bound R uxneg)). by rewrite /= bnd_simp. have [leuyly|-> ->|lyneg uyneg|lypos uypos|lyneg uypos] := interval_signP. + move=> + + /ltac:(exfalso); exact: empty10. + rewrite 2!bnd_simp => ley1 ley2. have -> : y = 0 by apply: le_anti; rewrite ley1 ley2. by rewrite mulr0 /Itv.itv_cond in_itv/= lexx. + move=> lelyy leyuy. have yneg : y <= 0. move: (le_trans leyuy (Itv.le_map_itv_bound R uyneg)). by rewrite /= bnd_simp. rewrite -[Interval _ _]/(Interval (mull (opp ux) (opp uy)) (mulr (opp lx) (opp ly))). rewrite -mulrNN /Itv.itv_cond itv_boundlr. rewrite mul_itv_boundl_subproof ?mul_itv_boundr_subproof //. * by rewrite bnd_simp oppr_ge0. * by rewrite bnd_simp oppr_ge0. * by rewrite opp_itv_boundr_subproof. * by rewrite opp_itv_boundr_subproof. * by rewrite opp_itv_ge0_subproof. * by rewrite opp_itv_ge0_subproof. * by rewrite opp_itv_boundl_subproof. * by rewrite opp_itv_boundl_subproof. + move=> lelyy leyuy. have ypos : 0 <= y. move: (le_trans (Itv.le_map_itv_bound R lypos) lelyy). by rewrite /= bnd_simp. rewrite -[Interval _ _]/(Interval (opp (mulr (opp lx) uy)) (opp (mull (opp ux) ly))). rewrite -[x * y]opprK -mulNr /Itv.itv_cond itv_boundlr. rewrite opp_itv_boundl_subproof opp_itv_boundr_subproof. rewrite mul_itv_boundl_subproof ?mul_itv_boundr_subproof //. * by rewrite bnd_simp oppr_ge0. * by rewrite opp_itv_boundr_subproof. * by rewrite opp_itv_ge0_subproof. * by rewrite opp_itv_boundl_subproof. + move=> lelyy leyuy. rewrite -[Interval _ _]/(Interval (opp (mulr (opp lx) uy)) (mulr (opp lx) (opp ly))). rewrite -[x * y]opprK -mulNr /Itv.itv_cond itv_boundlr. rewrite opp_itv_boundl_subproof -mulrN. rewrite 2?mul_itv_boundr'_subproof //. * by rewrite bnd_simp oppr_ge0. * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. * by rewrite opp_itv_boundr_subproof. * by rewrite opp_itv_boundr_subproof. * by rewrite bnd_simp oppr_ge0. * by rewrite ltW. * by rewrite opp_itv_boundr_subproof. - move=> lelxx lexux. have xpos : 0 <= x. move: (le_trans (Itv.le_map_itv_bound R lxpos) lelxx). by rewrite /= bnd_simp. have [leuyly|-> ->|lyneg uyneg|lypos uypos|lyneg uypos] := interval_signP. + move=> + + /ltac:(exfalso); exact: empty10. + rewrite 2!bnd_simp => ley1 ley2. have -> : y = 0 by apply: le_anti; rewrite ley1 ley2. by rewrite mulr0 /Itv.itv_cond in_itv/= lexx. + move=> lelyy leyuy. have yneg : y <= 0. move: (le_trans leyuy (Itv.le_map_itv_bound R uyneg)). by rewrite /= bnd_simp. rewrite -[Interval _ _]/(Interval (opp (mulr ux (opp ly))) (opp (mull lx (opp uy)))). rewrite -[x * y]opprK -mulrN /Itv.itv_cond itv_boundlr. rewrite opp_itv_boundl_subproof opp_itv_boundr_subproof. rewrite mul_itv_boundr_subproof ?mul_itv_boundl_subproof //. * by rewrite opp_itv_ge0_subproof. * by rewrite opp_itv_boundl_subproof. * by rewrite bnd_simp oppr_ge0. * by rewrite opp_itv_boundr_subproof. + move=> lelyy leyuy. have ypos : 0 <= y. move: (le_trans (Itv.le_map_itv_bound R lypos) lelyy). by rewrite /= bnd_simp. rewrite -[Interval _ _]/(Interval (mull lx ly) (mulr ux uy)). rewrite /Itv.itv_cond itv_boundlr. by rewrite mul_itv_boundr_subproof ?mul_itv_boundl_subproof. + move=> lelyy leyuy. rewrite -[Interval _ _]/(Interval (opp (mulr ux (opp ly))) (mulr ux uy)). rewrite -[x * y]opprK -mulrN /Itv.itv_cond itv_boundlr. rewrite opp_itv_boundl_subproof -mulrN opprK. rewrite 2?mul_itv_boundr'_subproof //. * by rewrite ltW. * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. * by rewrite opp_itv_boundr_subproof. - move=> lelxx lexux. have [leuyly|-> ->|lyneg uyneg|lypos uypos|lyneg uypos] := interval_signP. + move=> + + /ltac:(exfalso); exact: empty10. + rewrite 2!bnd_simp => ley1 ley2. have -> : y = 0 by apply: le_anti; rewrite ley1 ley2. by rewrite mulr0 /Itv.itv_cond in_itv/= lexx. + move=> lelyy leyuy. have yneg : y <= 0. move: (le_trans leyuy (Itv.le_map_itv_bound R uyneg)). by rewrite /= bnd_simp. rewrite -[Interval _ _]/(Interval (opp (mulr ux (opp ly))) (mulr (opp lx) (opp ly))). rewrite -[x * y]opprK -mulrN /Itv.itv_cond itv_boundlr. rewrite /mulr mul_itv_boundrC_subproof mulrC opp_itv_boundl_subproof. rewrite [in X in _ && X]mul_itv_boundrC_subproof -mulrN. rewrite mul_itv_boundr'_subproof ?mul_itv_boundr'_subproof //. * by rewrite bnd_simp oppr_ge0. * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. * by rewrite opp_itv_boundr_subproof. * by rewrite opp_itv_boundr_subproof. * by rewrite bnd_simp oppr_ge0. * by rewrite ltW. * by rewrite opp_itv_boundr_subproof. + move=> lelyy leyuy. have ypos : 0 <= y. move: (le_trans (Itv.le_map_itv_bound R lypos) lelyy). by rewrite /= bnd_simp. rewrite -[Interval _ _]/(Interval (opp (mulr (opp lx) uy)) (mulr ux uy)). rewrite -[x * y]opprK -mulNr /Itv.itv_cond itv_boundlr. rewrite /mulr mul_itv_boundrC_subproof mulrC opp_itv_boundl_subproof. rewrite [in X in _ && X]mul_itv_boundrC_subproof -mulrN opprK. rewrite mul_itv_boundr'_subproof ?mul_itv_boundr'_subproof //. * by rewrite ltW. * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. * by rewrite opp_itv_boundr_subproof. + move=> lelyy leyuy. rewrite -[Interval _ _]/(Interval (Order.min (opp (mulr (opp lx) uy)) (opp (mulr ux (opp ly)))) (Order.max (mulr (opp lx) (opp ly)) (mulr ux uy))). rewrite /Itv.itv_cond itv_boundlr. rewrite map_itv_bound_min map_itv_bound_max le_minl le_maxr. rewrite -[x * y]opprK !opp_itv_boundl_subproof. rewrite -[in X in ((X || _) && _)]mulNr -[in X in ((_ || X) && _)]mulrN. rewrite -[in X in (_ && (X || _))]mulrNN !opprK. have [xpos|xneg] := leP 0 x. * rewrite [in X in ((_ || X) && _)]mul_itv_boundr'_subproof ?orbT //=; rewrite ?[in X in (_ || X)]mul_itv_boundr'_subproof ?orbT //. - by rewrite ltW. - by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - by rewrite opp_itv_boundr_subproof. * rewrite [in X in ((X || _) && _)]mul_itv_boundr'_subproof //=; rewrite ?[in X in (X || _)]mul_itv_boundr'_subproof //. - by rewrite bnd_simp oppr_ge0 ltW. - by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - by rewrite opp_itv_boundr_subproof. - by rewrite opp_itv_boundr_subproof. - by rewrite bnd_simp oppr_ge0 ltW. - by rewrite ltW. - by rewrite opp_itv_boundr_subproof. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed