proposition: Lemma AbsIR_eq_x : forall x : IR, [0] [<=] x -> AbsIR x [=] x.
proof: Proof. intros. unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- *. apply eq_transitive_unfolded with (Max [--]x x). apply Max_comm. apply leEq_imp_Max_is_rht. apply leEq_transitive with ZeroR. 2: assumption. astepr ( [--]ZeroR). apply inv_resp_leEq. assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq