PosNum.ofNatSucc

Stream: mathlib4

[Ka Wing Li]

I am not sure if the following has been proven anywhere?

import Mathlib
lemma PostNum.cast_ofNat : ∀ n : Nat, (↑(PosNum.ofNat (n + 1)) : Nat) = n + 1 := by
  intros n; induction n
  case zero => simp [PosNum.ofNat, PosNum.ofNatSucc]
  case succ n ihn =>
    simp only [PosNum.ofNat, Nat.pred_eq_sub_one, add_tsub_cancel_right, PosNum.ofNatSucc,
      PosNum.cast_succ, Nat.add_right_cancel_iff]
    exact ihn

[Miyahara Kō]

Loogle is useful to search relevant lemmas.
According to the search result, docs#PosNum.ofNat has no lemmas.
As in the docstring, PosNum is basically unused and docs#PNat is more prefered, so it has poor API currently.

[Kim Morrison]

Yes, PosNum is a mostly vestigial structure, with very specialised use cases that have not seen any attention for a long time. I'd discourage adding anything to it.