proposition: Lemma zero_AbsSmall : forall e : R, [0] [<=] e -> AbsSmall e [0].
proof: Proof. intros. unfold AbsSmall in |- *. split. astepr ([--]ZeroR). apply inv_resp_leEq. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2