match hx : x.leNat n, hy : y.leNat n, hz : z.leNat n with
| true, true, true => trivial
| true, true, false => trivial
| true, false, true => trivial
| true, false, false => trivial
| false, true, true =>
  cases hxy n with
  | inl h => simp only [h] at hx
  | inr h => simp only [h] at hy
| false, true, false => trivial
| false, false, true =>
  cases hyz n with
  | inl h => simp only [h] at hy
  | inr h => simp only [h] at hz
| false, false, false => trivial
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
⊢ x.leNat n = true ∨ z.leNat n = false
no goals