proposition: Lemma AbsIR_pos : forall x : IR, x [#] [0] -> [0] [<] AbsIR x.
proof: Proof. intros. cut (x [<] [0] or [0] [<] x). 2: apply ap_imp_less; assumption. intros H0. unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- *. elim H0. intro. apply less_leEq_trans with ( [--]x). astepl ( [--]ZeroR). apply inv_resp_less. assumption. apply rht_leEq_Max. intro. apply less_leEq_trans with x. assumption. apply lft_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq