proposition: Lemma Rplus_pos_higher : forall {R : ConstructiveReals} (a eps:CRcarrier R), 0 < eps -> a < (a+eps).
proof: Proof. intros. rewrite <- (CRplus_0_r a). rewrite CRplus_assoc. apply CRplus_lt_compat_l. rewrite CRplus_0_l. exact H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal