proposition: Lemma LipschitzMin : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (k m : CRcarrier R), Lipschitz f k -> Lipschitz (fun x => CRmin m (f x)) k.
proof: Proof. intros R f k m fl x y. rewrite CRmin_sym, (CRmin_sym m). apply (CRle_trans _ _ _ (CRmin_contract _ _ _)). apply fl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal