Theorem rle_compat_mull

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, 3, 4, 5 ⊢ a⋅c ≤ b⋅c, rle_compat_mulr 1 2 3 4 5.
07. 1, 3 ⊢ c⋅a = a⋅c, rmul_comm 3 1.
08. 2, 3 ⊢ b⋅c = c⋅b, rmul_comm 2 3.
09. 1, 2, 3, 4, 5 ⊢ c⋅a ≤ b⋅c, eq_le_trans 7 6.
10. 1, 2, 3, 4, 5 ⊢ c⋅a ≤ c⋅b, le_eq_trans 9 8.
11. 1, 2, 3 ⊢ a ≤ b → 0 ≤ c → c⋅a ≤ c⋅b, subj_intro_ii 10.
rle_compat_mull. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a ≤ b → 0 ≤ c → c⋅a ≤ c⋅b, subj_intro_iii 11.

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.