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