no goals
m k : ℕ
⊢ psub m 0 = some k ↔ k + 0 = m
simp [eq_comm]
m n k : ℕ
⊢ (∃ a, psub m (Nat.add n 0) = some a ∧ ppred a = some k) ↔ k + (n + 1) = m
m n k : ℕ
⊢ psub m (n + 1) = some k ↔ k + (n + 1) = m
apply Option.bind_eq_some.trans
m n k : ℕ
⊢ (∃ a, a + Nat.add n 0 = m ∧ succ k = a) ↔ k + (n + 1) = m
m n k : ℕ
⊢ (∃ a, psub m (Nat.add n 0) = some a ∧ ppred a = some k) ↔ k + (n + 1) = m
simp only [psub_eq_some, ppred_eq_some]
no goals
m n k : ℕ
⊢ (∃ a, a + Nat.add n 0 = m ∧ succ k = a) ↔ k + (n + 1) = m
simp [add_comm, add_left_comm, Nat.succ_eq_add_one]