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