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