m n : ℕ
⊢ Option.getD (ppred (Option.getD (psub m n) 0)) 0 = Option.getD (psub m n >>= ppred) 0
m n : ℕ
⊢ Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
rw [sub_eq_psub m n, psub]
no goals
m n : ℕ
⊢ Option.getD (ppred (Option.getD (psub m n) 0)) 0 = Option.getD (psub m n >>= ppred) 0
cases psub m n <;> rfl