proposition: Lemma leEq_AbsIR : forall x : IR, x [<=] AbsIR x.
proof: Proof. intros. unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- *; apply lft_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq