proposition: Lemma IR_AbsSmall_as_CR : forall (x y:IR), AbsSmall x y <-> AbsSmall (R:=CRasCOrdField) (IRasCR x) (IRasCR y).
proof: Proof. unfold AbsSmall. intros x y. simpl. do 2 rewrite -> IR_leEq_as_CR. rewrite -> IR_opp_as_CR. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac