contradiction
case negSucc
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
prop : Int.abs (Int.negSucc n) < nrows t
h : { val := Int.negSucc n, property := prop }.val ≥ 0
hcontra : Int.negSucc n < 0
⊢ False
no goals