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