proposition: Lemma mult_AbsSmall_lft : forall x y X Y : R, [0] [<=] X -> [0] [<=] Y -> [--]X [<=] x -> x [<=] X -> [--]Y [<=] y -> y [<=] Y -> [--](X[*]Y) [<=] x[*]y.
proof: Proof. intros. rstepr ([--]([--]x[*]y)). apply inv_resp_leEq. apply mult_AbsSmall_rht; auto. apply inv_resp_leEq. auto. rstepr ([--][--]X). apply inv_resp_leEq. auto. Qed.
imports: CoRN.algebra.COrdFields2