proposition: Lemma approach_zero : forall x : R, (forall e, [0] [<] e -> x [<] e) -> x [<=] [0].
proof: Proof. intros. rewrite -> leEq_def; intro. cut (x [<] x [/]TwoNZ). change (Not (x [<] x [/]TwoNZ)) in |- *. apply less_antisymmetric_unfolded. 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 X. apply pos_div_two. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)