fact: Definition mul_itv_subdef (i1 i2 : interval int) : interval int := let 'Interval l1 u1 := i1 in let 'Interval l2 u2 := i2 in let opp := opp_itv_bound_subdef in let mull := mul_itv_boundl_subdef in let mulr := mul_itv_boundr_subdef in match interval_sign i1, interval_sign i2 with | None, _ | _, None => `[1, 0] | some s1, Some s2 => (match s1, s2 with | =0, _ => `[0, 0] | _, =0 => `[0, 0] | >=0, >=0 => Interval (mull l1 l2) (mulr u1 u2) | <=0, <=0 => Interval (mull (opp u1) (opp u2)) (mulr (opp l1) (opp l2)) | >=0, <=0 => Interval (opp (mulr u1 (opp l2))) (opp (mull l1 (opp u2))) | <=0, >=0 => Interval (opp (mulr (opp l1) u2)) (opp (mull (opp u1) l2)) | >=0, >=<0 => Interval (opp (mulr u1 (opp l2))) (mulr u1 u2) | <=0, >=<0 => Interval (opp (mulr (opp l1) u2)) (mulr (opp l1) (opp l2)) | >=<0, >=0 => Interval (opp (mulr (opp l1) u2)) (mulr u1 u2) | >=<0, <=0 => Interval (opp (mulr u1 (opp l2))) (mulr (opp l1) (opp l2)) | >=<0, >=<0 => Interval (Order.min (opp (mulr (opp l1) u2)) (opp (mulr u1 (opp l2)))) (Order.max (mulr (opp l1) (opp l2)) (mulr u1 u2)) end)%snum_sign end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed