Theorem rdiv_dist_sub

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_sub 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_sub. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  ¬c = 0 → (a - b)/c = a/c - b/c, subj_intro_iv 12.

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