proposition: Lemma MAbs_one : forall F : CMetricField, {MAbs ([1]:F) [=] [0]} + {MAbs ([1]:F) [=] [1]}.
proof: Proof. intro F. apply square_id. astepl (cmf_abs F [1][*]cmf_abs F [1]). astepl (cmf_abs F ([1][*][1])). astepl (cmf_abs F [1]). apply eq_reflexive. apply ax_abs_resp_mult. apply cmf_proof. Qed.
imports: CoRN.reals.CReals1