Proof nmul_distr_add. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → (a + b)⋅c = a⋅c + b⋅c, pred_iii_restr nat_incl_in_real rmul_distr_add.
Dependencies
The given proof depends on seven axioms:
comp, eq_refl, eq_subst, radd_closed, real_is_set, rmul_comm, rmul_distl_add.