Theorem rle_compat_mulr

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a ≤ b, hypo.
05. 5 ⊢ 0 ≤ c, hypo.
06. 1, 2, 4 ⊢ 0 ≤ b - a, rle_as_diff 1 2 4.
07. 1, 2 ⊢ b - a ∈ ℝ, rsub_closed 2 1.
08. 1, 2, 3, 4, 5 ⊢ 0 ≤ (b - a)⋅c, rle_compat_mul 7 3 6 5.
09. 1, 2, 3 ⊢ (b - a)⋅c = b⋅c - a⋅c, rmul_distr_sub 2 1 3.
10. 1, 2, 3, 4, 5 ⊢ 0 ≤ b⋅c - a⋅c, le_eq_trans 8 9.
11. 1, 3 ⊢ a⋅c ∈ ℝ, rmul_closed 1 3.
12. 2, 3 ⊢ b⋅c ∈ ℝ, rmul_closed 2 3.
13. 1, 2, 3, 4, 5 ⊢ a⋅c ≤ b⋅c, rle_from_diff 11 12 10.
14. 1, 2, 3 ⊢ a ≤ b → 0 ≤ c → a⋅c ≤ b⋅c, subj_intro_ii 13.
rle_compat_mulr. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a ≤ b → 0 ≤ c → a⋅c ≤ b⋅c, subj_intro_iii 14.

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