fact: Definition gamma02 x t := (f x t + c/2 * RInt (fun tau => Derive (fun u => f u tau) (x + c * (t - tau)) - Derive (fun u => f u tau) (x - c * (t - tau))) 0 t).
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)