proposition: Lemma AbsIR_nonneg : forall x : IR, [0] [<=] AbsIR x.
proof: Proof. intro x; rewrite -> leEq_def; intro H. cut ([0] [<] ZeroR). apply less_irreflexive. apply less_wdl with (AbsIR x); auto. eapply eq_transitive_unfolded. 2: apply AbsIRz_isz. apply AbsIR_wd. unfold AbsIR in H; simpl in H; unfold ABSIR in H. apply leEq_imp_eq; apply less_leEq. apply leEq_less_trans with (Max x [--]x). apply lft_leEq_Max. assumption. apply inv_cancel_less. apply leEq_less_trans with (Max x [--]x). apply rht_leEq_Max. astepr ZeroR; auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq