contradiction
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 2 ≤ n✝ + 1 + 1
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 2 ≤ n✝ + 1 + 1