proposition: Lemma MAbs_one_recip_one : forall F : CMetricField, MAbs ([1]:F) [=] MAbs ( [--][1]:F).
proof: Proof. intro F. cut ({cmf_abs F ([1]:F) [=] [0]} + {cmf_abs F ([1]:F) [=] [1]}). intro H. elim H. intro H2. astepl ZeroR. astepr (cmf_abs F ( [--][1][*][1])). astepr (cmf_abs F [--][1][*]cmf_abs F [1]). astepr (cmf_abs F [--][1][*][0]). astepr ZeroR. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply ax_abs_resp_mult. apply cmf_proof. intro H1. cut (cmf_abs F [--][1] [=] cmf_abs F [1] or cmf_abs F [--][1] [=] [--] (cmf_abs F [1])). intro H2. elim H2. intro H3. apply eq_symmetric_unfolded. exact H3. intro H3. Lemma Hulp : forall F : CMetricField, cmf_abs F [1] [=] [1] -> cmf_abs F [--][1] [=] [--] (cmf_abs F [1]) -> False. intros F G H. set (H0 := ax_abs_gt_zero) in *. generalize H0. intro H1. set (H2 := H1 F (cmf_abs F) (cmf_proof F) [--] ([1]:F)) in *. rewrite -> leEq_def in H2. apply H2. astepl ( [--] (cmf_abs F [1])). astepl ( [--]OneR). apply plus_cancel_less with OneR. astepl ZeroR. astepr OneR. apply pos_one. Qed.
imports: CoRN.reals.CReals1