proposition: Lemma CompactCompleteCompact_uc : is_UniformlyContinuousFunction CompactCompleteCompact_fun Qpos2QposInf.
proof: Proof. intros e a b H d1 d2. simpl in *. apply (@FinCompact_uc (d1+e+d2)%Qpos). apply H. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround CoRN.metric2.Prelength