proposition: Lemma plus_resp_less_both : forall a b c d : R, a [<] b -> c [<] d -> a[+]c [<] b[+]d.
proof: Proof. intros. apply less_leEq_trans with (a[+]d). apply plus_resp_less_lft. assumption. apply less_leEq. apply plus_resp_less_rht. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)