proposition: Lemma MSequivalent_discr : Not (MSequivalent IR_as_CPsMetricSpace (zf_as_CPsMetricSpace IR)).
proof: Proof. red in |- *. unfold MSequivalent in |- *. unfold isopsmetry in |- *. unfold equivalent_psmetric in |- *. intros H0. elim H0. intros f H0'. elim H0'. intros H1 H2. elim H2. intros H3 H4. elim H4. intros H5 H6. elim H5. intros n. simpl in |- *. unfold zero_fun in |- *. unfold dIR in |- *. intro H7. cut (OneR[<=][0]). rewrite -> leEq_def in |- *. intro H8. set (H9 := H8 (pos_one IR)) in *. exact H9. astepr ((nring (R:=IR) n[+][1])[*][0]). astepl (ABSIR ([1][-][0])). apply H7. unfold ABSIR in |- *. astepl (Max [--]([1][-][0]) ([1][-][0])). astepl (Max [--]([1][-][0]) [1]). apply leEq_imp_Max_is_rht. astepl ([--]OneR). astepl (ZeroR[-][1]). apply shift_minus_leEq. astepr (Two:IR). apply less_leEq. apply pos_two. apply Max_comm. Qed.
imports: CoRN.metrics.IR_CPMSpace