proposition: Lemma leEq_transitive : forall x y z : R, x [<=] y -> y [<=] z -> x [<=] z.
proof: Proof. intros x y z. repeat rewrite -> leEq_def. intros H H0 H1. apply H. apply leEq_less_trans with (y := z); firstorder using leEq_def. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)