proposition: Lemma regFunEq_equiv : forall (x y : Complete), regFunEq x y <-> msp_eq x y.
proof: Proof. unfold regFunEq, msp_eq. split. - intros H e1 e2. rewrite Qplus_0_r. apply H. - intros H e1 e2. specialize (H e1 e2). rewrite Qplus_0_r in H. apply H. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax