proposition: Lemma plus_resp_less_lft : forall x y z : R, x [<] y -> z[+]x [<] z[+]y.
proof: Proof. intros x y z H. astepl (x[+]z). astepr (y[+]z). apply plus_resp_less_rht. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)