Two lemmas on choose

The proofs of these lemmas use the ring tactic and can't be given in Mathlib.Data.Nat.Choose.Basic

theorem Nat.choose_mul_add {m n : ℕ} (hn : n ≠ 0) : (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)

theorem Nat.choose_mul_right {m n : ℕ} (hn : n ≠ 0) : (m * n).choose n = m * (m * n - 1).choose (n - 1)