proposition: Lemma AbsSmall_trans : forall e1 e2 d : R, e1 [<] e2 -> AbsSmall e1 d -> AbsSmall e2 d.
proof: Proof. intros. apply AbsSmall_leEq_trans with e1. apply less_leEq. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2