refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i = List.length l
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i ≤ List.length l