proposition: Lemma eps2_Rgt_R0 : forall {R : ConstructiveReals} (eps : CRcarrier R), 0 < eps -> 0 < eps * CR_of_Q R (1#2).
proof: Proof. intros. apply CRmult_lt_0_compat. apply H. apply CR_of_Q_pos; reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal