Axiom rle_compat_mul
Axiom.
rle_compat_mul
a ∈ ℝ → b ∈ ℝ → 0 ≤ a → 0 ≤ b → 0 ≤ a⋅b