proposition: Lemma mult_resp_AbsSmall: forall (R: COrdField) (x y e : R) (H: [0][<=]y), AbsSmall e x -> AbsSmall (y[*]e) (y[*]x).
proof: Proof. unfold AbsSmall. intros. destruct H0. split. rstepl (y[*]([--]e)). apply mult_resp_leEq_lft; auto. apply mult_resp_leEq_lft; auto. Qed.
imports: CoRN.algebra.COrdFields2