proposition: Lemma approach_zero_weak : forall x : R, (forall e, [0] [<] e -> x [<=] e) -> x [<=] [0].
proof: Proof. intros. rewrite -> leEq_def; intro. cut (x [<=] x [/]TwoNZ). rewrite -> leEq_def. change (~ Not (x [/]TwoNZ [<] x)) in |- *. intro H1. apply H1. apply plus_cancel_less with (z := [--](x [/]TwoNZ)). apply mult_cancel_less with (z := Two:R). apply pos_two. rstepl ([0]:R). rstepr x. assumption. apply H. apply pos_div_two. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)