proposition: Lemma ABSIR_strext : un_op_strext _ ABSIR.
proof: Proof. unfold un_op_strext in |- *. unfold fun_strext in |- *. unfold ABSIR in |- *. intros. generalize (csbf_strext _ _ _ Max); intro H0. unfold bin_fun_strext in H0. generalize (H0 _ _ _ _ X); intro H1. elim H1. intro H2. assumption. intro H2. apply zero_minus_apart. generalize (minus_ap_zero _ _ _ H2); intro H3. generalize (inv_resp_ap_zero _ _ H3); intro H4. cut (x[-]y [=] [--] ( [--]x[-][--]y)). intro. astepl ( [--] ( [--]x[-][--]y)). auto. rational. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq