Lemmas about nonzero elements of an AddMonoidWithOne

theorem NeZero.one_le {n : ℕ} [NeZero n] : 1 ≤ n

theorem NeZero.natCast_ne (n : ℕ) (R : Type u_1) [AddMonoidWithOne R] [h : NeZero ↑n] : ↑n ≠ 0

theorem NeZero.of_neZero_natCast (R : Type u_1) [AddMonoidWithOne R] {n : ℕ} [h : NeZero ↑n] : NeZero n

theorem NeZero.pos_of_neZero_natCast (R : Type u_1) [AddMonoidWithOne R] {n : ℕ} [NeZero ↑n] : 0 < n