proposition: Lemma CSUCTrapezePlateau : forall {R : ConstructiveReals} (a b eta x : CRcarrier R) (etaPos : 0 < eta), (a <= x <= b) -> CSUCUnitTrapeze a b eta etaPos x == 1.
proof: Proof. intros. unfold CSUCUnitTrapeze. rewrite UCHeavisideIn. 2: apply H. unfold UCUnitHeaviside. rewrite CRmax_left. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. apply (CRle_trans _ _ _ (CRmin_r _ _)). apply (CRmult_le_reg_r (b+eta-b)). unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. apply etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_0_l, CRmult_1_r. unfold CRminus. rewrite CRplus_comm. rewrite <- (CRplus_opp_l b). apply CRplus_le_compat_l. apply H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal