fact: Record is_COrdField (F : CField) (less : CCSetoid_relation F) (leEq : Relation F) (greater : CCSetoid_relation F) (grEq : Relation F) : CProp := {ax_less_strorder : strictorder less; ax_plus_resp_less : forall x y, less x y -> forall z, less (x[+]z) (y[+]z); ax_mult_resp_pos : forall x y, less [0] x -> less [0] y -> less [0] (x[*]y); ax_less_conf_ap : forall x y, Iff (x [#] y) (less x y or less y x); def_leEq : forall x y, (leEq x y) <-> (Not (less y x)); def_greater : forall x y, Iff (greater x y) (less y x); def_grEq : forall x y, (grEq x y) <-> (leEq y x)}.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)