proposition: Lemma less_antisymmetric_unfolded : forall x y : F, x [<] y -> Not (y [<] x).
proof: Proof. elim less_strorder. intros H1 H2 x y H. intro H0. elim (H2 _ _ H). assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)