proposition: Lemma TrapezeLe : forall {R : ConstructiveReals} (a b eta : CRcarrier R) (etaPos : 0 < eta), a <= b -> a-eta <= b+eta.
proof: Proof. intros. apply (CRle_trans _ (a-0)). apply CRplus_le_compat_l, CRopp_ge_le_contravar, CRlt_asym, etaPos. unfold CRminus. rewrite CRopp_0. apply CRplus_le_compat. exact H. apply CRlt_asym, etaPos. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont