exact Nat.le_trans hle (Nat.le_succ ..)
case left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1
no goals