proposition: Lemma fasterIsEq : msp_eq faster x.
proof: Proof. apply regFunEq_equiv. apply regFunEq_e. intros e. simpl. apply ball_weak_le with (proj1_sig (f e + e)%Qpos). simpl. apply Qplus_le_l. apply Hf. apply regFun_prf. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax