proposition: Lemma COrdField_is_COrdField : is_COrdField F cof_less (@cof_leEq F) cof_greater (@cof_grEq F).
proof: Proof. elim F; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)