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