proposition: Lemma AbsSmall_wdl_unfolded : forall x y z : R, AbsSmall x y -> x [=] z -> AbsSmall z y.
proof: Proof. Proof AbsSmall_wdl. Declare Left Step AbsSmall_wdl_unfolded. Declare Right Step AbsSmall_wdr_unfolded. Notation ZeroR := ([0]:R). Lemma AbsSmall_leEq_trans : forall e1 e2 d : R, e1 [<=] e2 -> AbsSmall e1 d -> AbsSmall e2 d. Proof. unfold AbsSmall in |- *. intros. elim H0; intros. split. apply leEq_transitive with ([--]e1). apply inv_resp_leEq. assumption. assumption. apply leEq_transitive with e1. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields2