proposition: Lemma inv_resp_AbsSmall : forall x y : R, AbsSmall x y -> AbsSmall x [--]y.
proof: Proof. unfold AbsSmall in |- *. intros. elim H; intros. split. apply inv_resp_leEq. assumption. astepr ([--][--]x). apply inv_resp_leEq. assumption. Qed.
imports: CoRN.algebra.COrdFields2