sub one succ

Stream: Is there code for X?

[Bolton Bailey]

I'm looking for this lemma, is it in mathlib?

lemma nat.sub_one_succ (n : ℕ) (h : 0 < n) : nat.succ (n-1) = n :=
begin
  library_search,
end

[Eric Rodriguez]

docs#nat.succ_pred_eq_of_pos