Theorem: Nat.isUnitFactorial (DividedPowers/RatAlgebra.lean)

State before:
n : ℕ
⊢ IsUnit ↑n !
Tactic:
rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
State after:
n : ℕ
⊢ ¬n ! = 0

State before:
n : ℕ
⊢ ¬n ! = 0
Tactic:
apply Nat.factorial_ne_zero
State after:
no goals