fact: Definition UCUnitHeaviside {R : ConstructiveReals} (a b : CRcarrier R) (ltab : a < b) : CRcarrier R -> CRcarrier R := fun x => (CRmax 0 (CRmin 1 ((x - a) * (CRinv R (b-a) (inr (CRlt_minus _ _ ltab)))))).
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal