proposition: Lemma less_irreflexive_unfolded : forall x : F, Not (x [<] x).
proof: Proof. Proof less_irreflexive. Lemma plus_resp_less_rht : forall x y z : F, x [<] y -> x[+]z [<] y[+]z. Proof. elim COrdField_is_COrdField; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)