case h
n m : ℕ
x y : Fin (n + 1)
h : x < y
hy : optParam (y ≠ 0) (_ : y ≠ 0)
⊢ x ≤ ↑castSucc (pred y hy)
n m : ℕ
x y : Fin (n + 1)
h : x < y
hy : optParam (y ≠ 0) (_ : y ≠ 0)
⊢ ↑(succAbove x) (pred y hy) = y
rw [succAbove_above, succ_pred]
no goals
case h
n m : ℕ
x y : Fin (n + 1)
h : x < y
hy : optParam (y ≠ 0) (_ : y ≠ 0)
⊢ x ≤ ↑castSucc (pred y hy)
simpa [le_iff_val_le_val] using Nat.le_pred_of_lt h