proposition: Lemma AbsSmall_reflexive : forall (e : R), [0] [<=] e -> AbsSmall e e.
proof: Proof. intros. unfold AbsSmall. split. apply leEq_transitive with ([0]:R); auto. astepr ([--][0]:R). apply inv_resp_leEq. auto. apply leEq_reflexive. Qed.
imports: CoRN.algebra.COrdFields2