proposition: Lemma mult_resp_less_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_less. assumption. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)