[Merged by Bors] - chore: deal with erw
in Mathlib.Data.PNat.Interval
#17568
+4
−20
erw
in Mathlib.Data.PNat.Interval
#17568