proposition: Lemma less_leEq : forall x y : R, x [<] y -> x [<=] y.
proof: Proof. intros. rewrite -> leEq_def. apply less_antisymmetric_unfolded. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)