no goals
m : ℕ
⊢ ppred 0 = some m ↔ succ m = 0
constructor <;> intro h <;> contradiction
no goals
m n : ℕ
⊢ ppred (n + 1) = some m ↔ succ m = n + 1
constructor <;> intro h <;> injection h <;> subst m <;> rfl