proposition: Lemma UC_x : forall {R : ConstructiveReals}, UniformCont (fun x:CRcarrier R => x) (fun eps _ => eps).
proof: Proof. split. intros. exact xPos. intros. exact H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal