2 goals
p q : Prop,
Hp : p
⊢ q ∨ p

p q : Prop,
Hq : q
⊢ q ∨ p
-----
2 goals
⊢ 0 = 0 ∨ 0 = succ (pred 0)

n' : ℕ,
Hind : n' = 0 ∨ n' = succ (pred n')
⊢ succ n' = 0 ∨ succ n' = succ (pred (succ n'))
-----
2 goals
H : 0 ≠ 0
⊢ 0 > 0 → 0 = succ (pred 0)

n_n : ℕ,
n_ih : n_n ≠ 0 → n_n > 0 → n_n = succ (pred n_n),
H : succ n_n ≠ 0
⊢ succ n_n > 0 → succ n_n = succ (pred (succ n_n))
