proposition: Lemma less_irreflexive : irreflexive (cof_less (c:=F)).
proof: Proof. red in |- *. intro x; intro H. elim (less_antisymmetric_unfolded _ _ H H). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)