Theorem nmul_distr_sub

Proof
nmul_distr_sub. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → (a - b)⋅c = a⋅c - b⋅c,
  pred_iii_restr nat_incl_in_real rmul_distr_sub.

Dependencies
The given proof depends on 13 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, real_is_set, rmul_closed, rmul_comm, rmul_distl_add, rneg_closed.