English
If casts to α agree and α has characteristic zero, then the original PosNum are equal.
Русский
Если два PosNum при приведении в α дают одинаковые значения и α имеет характеристику ноль, то эти PosNum равны.
LaTeX
$$$[AddMonoidWithOne \\alpha] [CharZero \\alpha] \\{m,n : \\text{PosNum}\\} : (m : \\alpha) = (n : \\alpha) \\iff m = n$$$
Lean4
@[simp, norm_cast]
theorem cast_inj [AddMonoidWithOne α] [CharZero α] {m n : PosNum} : (m : α) = n ↔ m = n := by
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]