proposition: Lemma mult_resp_leEq_lft : forall x y z : R, x [<=] y -> [0] [<=] z -> z[*]x [<=] z[*]y.
proof: Proof. intros. astepl (x[*]z). astepr (y[*]z). apply mult_resp_leEq_rht. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)