proposition: Lemma AbsSmall_approach_zero : forall x : R, (forall e, [0] [<] e -> AbsSmall e x) -> x [=] [0].
proof: Proof. intros. apply not_ap_imp_eq. intro H0. elim (ap_imp_less _ _ _ H0). change (Not (x [<] [0])). rewrite <- leEq_def. apply inv_cancel_leEq. astepr ZeroR. apply approach_zero_weak. intros. apply inv_cancel_leEq; astepr x. elim (H e); auto. change (Not ([0] [<] x)). rewrite <- leEq_def. apply approach_zero_weak. intros. elim (H e); auto. Qed.
imports: CoRN.algebra.COrdFields2