proposition: Lemma leEq_wdr : forall x y z : R, x [<=] y -> y [=] z -> x [<=] z.
proof: Proof. intros x y z H H0. rewrite -> leEq_def in *. intro H1. apply H. astepl z; assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)