fact: Definition DiracOneFunc {R : ConstructiveReals} : @PartialFunction R (CRcarrier R) := Build_PartialFunctionXY (CRcarrier R) (CRcarrier R) (CReq R) (fun x => x == 0) (fun x xD => 1) (fun x p q => CReq_refl _).
imports: QArith ConstructiveReals ConstructiveLimits ConstructiveAbs ConstructiveMinMax ConstructivePartialFunctions CMTbase