Theorem rdiv_dist_add

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ ¬c = 0, hypo.
05. 3, 4 ⊢ /c ∈ ℝ, rinv_closed 3 4.
06. ⊢ (a + b)/c = (a + b)⋅(/c), rdiv_eq.
07. 1, 2, 3, 4 ⊢ (a + b)⋅(/c) = a⋅(/c) + b⋅(/c),
  rmul_distr_add 1 2 5.
08. 1, 2, 3, 4 ⊢ (a + b)/c = a⋅(/c) + b⋅(/c), eq_trans 6 7.
09. ⊢ a/c = a⋅(/c), rdiv_eq.
10. ⊢ b/c = b⋅(/c), rdiv_eq.
11. ⊢ a/c + b/c = a⋅(/c) + b⋅(/c),
  eq_cong_ii 9 10, f x y = x + y.
12. 1, 2, 3, 4 ⊢ (a + b)/c = a/c + b/c, eq_trans_rr 8 11.
rdiv_dist_add. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  ¬c = 0 → (a + b)/c = a/c + b/c, subj_intro_iv 12.

Dependencies
The given proof depends on six axioms:
eq_refl, eq_subst, radd_closed, rinv_closed, rmul_comm, rmul_distl_add.