proposition: Lemma leEq_less_trans : forall x y z : R, x [<=] y -> y [<] z -> x [<] z.
proof: Proof. intros x y z. intros H H0. elim (less_cotransitive_unfolded _ _ _ H0 x); intro H1; try assumption. destruct (leEq_def _ x y) as [H2 H3]. elim ((H2 H) H1). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)