proposition: Lemma AbsSmall_nonneg : forall e x : R, AbsSmall e x -> [0] [<=] e.
proof: Proof. unfold AbsSmall in |- *. intros. elim H. intros. cut ([--]e [<=] e). intros. apply mult_cancel_leEq with (z := Two:R). apply pos_two. apply plus_cancel_leEq_rht with (z := [--]e). rstepl ([--]e). rstepr e. assumption. apply leEq_transitive with (y := x). assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2