Real_Number_Ordering_Compatible_with_Mult
ProvedFor non-negative reals, multiplication preserves ordering.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Real_Number_Ordering_Compatible_with_Mult (a b c : ℝ) (ha : 0 ≤ a) (hbc : b ≤ c) : a * b ≤ a * c := by sorry