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