proposition: Lemma UCHeavisideBounded : forall {R : ConstructiveReals} (a b x : CRcarrier R) (ltab : a < b), (0 <= UCUnitHeaviside a b ltab x <= 1).
proof: Proof. intros. unfold UCUnitHeaviside. split. - apply CRmax_l. - apply CRmax_lub. apply CRlt_asym, CRzero_lt_one. apply CRmin_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal