proposition: Lemma UC_constant : forall {R : ConstructiveReals} (c : CRcarrier R), UniformCont (fun _:CRcarrier R => c) (fun _ _ => 1).
proof: Proof. split. intros. apply CRzero_lt_one. intros. unfold CRminus. rewrite CRplus_opp_r, CRabs_right. exact epsPos. apply CRle_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal