cases z with | mk z prop =>
simp only [head]
have h_not_neg : ¬ (z < 0) := by
  intro hcontra
  cases z with
  | ofNat n => contradiction
  | negSucc n => contradiction
simp only [ite_false, h_not_neg]
simp only [List.take, nrows, Schema.length_eq_List_length]
rw [List.length_take]
. exact Int.toNat_of_ofNat_inj z h
. unfold nrows at prop
  rw [Int.abs_of_nonneg_eq_toNat] at prop
  . exact Schema.length_eq_List_length ▸ prop
  . exact h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : { z // Int.abs z < nrows t }
h : z.val ≥ 0
⊢ Int.ofNat (nrows (head t z.val)) = z.val
no goals