proposition: Lemma regFunBall_Cunit (e: Qpos) (x: Complete) (y: X): regFunBall (proj1_sig e) x (Cunit y) <-> (forall d: Qpos, ball (proj1_sig d + proj1_sig e) (approximate x d) y).
proof: Proof. Proof with auto. unfold regFunBall. split; intros. apply ball_closed. simpl in *... intros. apply (H d (exist _ _ H0)). apply ball_weak... apply Qpos_nonneg. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax