fact: Definition CSUCUnitTrapeze {R : ConstructiveReals} (a b eta : CRcarrier R) (etaPos : 0 < eta) (x : CRcarrier R) : CRcarrier R := UCUnitHeaviside (a-eta) a (Rminus_pos_lower a eta etaPos) x - UCUnitHeaviside b (b+eta) (Rplus_pos_higher b eta etaPos) x.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal