field_simp with factorials in Lean: supply (n ! : ℚ) ≠ 0 explicitly

For a factorial recurrence in ℚ (e.g. super Catalan f(m,n) = (2m)!(2n)!/(m!n!(m+n)!), with f(m,n+1) = 4f(m,n) - f(m+1,n)), first rewrite 2*(n+1) to 2*n+1+1, then simp only [Nat.factorial_succ] and push_cast. field_simp does NOT clear the factorial denominators on its own. Add have : (m ! : ℚ) ≠ 0 := by exact_mod_cast (Nat.factorial_pos m).ne' for each factorial, plus ((m:ℚ)+n+1) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero _. positivity failed on these casts in a module file with minimal imports. After that, field_simp; ring closes the goal. For integrality, induct on n for all m (∃ z : ℤ, f m n = z), with base f(m,0) = C(2m,m) via Nat.cast_choose.