cases Nat.le_total n n₀ with
| inl h => right; exact mono' h hy
| inr h => left; exact mono h hx
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
⊢ x.leNat n = true ∨ y.leNat n = false
no goals