fact: Definition midpoint xi := match xi with | Inan => F.zero | Ibnd xl xu => match F.real xl, F.real xu with | false, false => F.zero | true, false => match F.cmp xl F.zero with | Xund | Xlt => F.zero | Xeq => c1 | Xgt => let m := F.mul_UP p52 xl c2 in if F.real m then m else xl end | false, true => match F.cmp xu F.zero with | Xund | Xgt => F.zero | Xeq => cm1 | Xlt => let m := F.mul_DN p52 xu c2 in if F.real m then m else xu end | true, true => F.midpoint xl xu end end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval