Proof nmul_distl_sub. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a⋅(b - c) = a⋅b - a⋅c, pred_iii_restr nat_incl_in_real rmul_distl_sub.
Dependencies
The given proof depends on 12 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, real_is_set, rmul_closed, rmul_distl_add, rneg_closed.