fact: Definition midpoint (x y : type) := let z := ((x + y) / 2)%float in if is_infinity z then (x / 2 + y / 2)%float else z.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig