theorem CharP.addOrderOf_natCast {R : Type u_1} [AddGroupWithOne R] (p : ℕ) [CharP R p] {n : ℕ} (hn : n ≠ 0) : addOrderOf ↑n = p / p.gcd n