exfalso
case inl
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : Int.toNat (-n) = 0
⊢ 1 ≤ Int.toNat (-n)

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s1 : Int.toNat (-n) = 0
⊢ False

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
s2 : Int.toNat (-n) > 0
⊢ 1 ≤ Int.toNat (-n)