proposition: Lemma less_leEq_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 _ _ _ H z); intro H1. assumption. destruct (leEq_def _ y z). elim ((H2 H0) H1). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)