Transitivity for LE on Nat #
We rewrite inequalities for natural numbers using transitivity. Namely, if the goal is a ≤ b and we have a ≤ c, we can rewrite the goal to c ≤ b and similarly for c ≤ b and for just a ≤ b.
Equations
- One or more equations did not get rendered due to their size.