proposition: Lemma leEq_reflexive : forall x : R, x [<=] x.
proof: Proof. intro x. rewrite -> leEq_def. apply less_irreflexive_unfolded. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)