fact: Definition point_in_holed_interval (a b h : R) : R := if Req_dec_T h (Rdiv (Rplus a b) (INR 2)) then (Rdiv (Rplus a h) (INR 2)) else (Rdiv (Rplus a b) (INR 2)).
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon