11 lines
162 B
Text
11 lines
162 B
Text
|
LEAN_INFORMATION
|
|||
|
|
a b c d : ℕ,
|
|||
|
|
h₁ : a + b = 0,
|
|||
|
|
h₂ : b = 0,
|
|||
|
|
aeq0 : a = 0,
|
|||
|
|
h₃ : c + 1 + a = 1,
|
|||
|
|
h₄ : d = c - 1,
|
|||
|
|
deq0 : d = 0
|
|||
|
|
⊢ d = 0
|
|||
|
|
END_LEAN_INFORMATION
|