rw [List.length_take]
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.ofNat (List.length (List.take (Int.toNat z) t.rows)) = z
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.ofNat (Int.toNat z) = z

case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows