proposition: Lemma mult_resp_less : forall x y z : R, x [<] y -> [0] [<] z -> x[*]z [<] y[*]z.
proof: Proof. intros. apply plus_cancel_less with ([--](x[*]z)). astepl ([0]:R). rstepr ((y[-]x)[*]z). apply mult_resp_pos. astepl (x[-]x). apply minus_resp_less. assumption. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)