case zero
m n : ℕ
⊢ psub m (n + zero) = do
    let __do_lift ← psub m n
    psub __do_lift zero

case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
m n k : ℕ
⊢ psub m (n + k) = do
    let __do_lift ← psub m n
    psub __do_lift k
induction k
case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
case zero
m n : ℕ
⊢ psub m (n + zero) = do
    let __do_lift ← psub m n
    psub __do_lift zero

case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
simp [Option.bind_eq_bind, Option.bind_some]
no goals
case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
simp [*, Nat.add_succ]