rw [List.length_reverse, List.length_drop, List.length_reverse]
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ List.length (List.reverse (List.drop (Int.abs z) (List.reverse t.rows))) = List.length t.rows - Int.abs z
case mk.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ Int.abs z < List.length (List.reverse t.rows)