proposition: Lemma UCHeavisideIn : forall {R : ConstructiveReals} (a b x : CRcarrier R) (altb : a < b), b <= x -> UCUnitHeaviside a b altb x == 1.
proof: Proof. intros. unfold UCUnitHeaviside. rewrite CRmin_left, CRmax_right. reflexivity. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r (b-a)). unfold CRminus. rewrite <- (CRplus_opp_r a). apply CRplus_lt_compat_r. exact altb. rewrite CRmult_assoc, CRinv_l, CRmult_1_l, CRmult_1_r. unfold CRminus. rewrite CRplus_comm, (CRplus_comm x). apply CRplus_le_compat_l. apply H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal