Linearly ordered commutative groups and monoids with a zero element adjoined

In this file we provide some basic inequality results for groups with zero.

theorem mul_inv_lt_iff₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (hc : c ≠ 0) : a * c⁻¹ < b ↔ a < b * c

theorem inv_mul_lt_iff₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (hc : c ≠ 0) : c⁻¹ * a < b ↔ a < b * c

theorem inv_mul_lt_one_iff₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {c : α} (hc : c ≠ 0) : c⁻¹ * a < 1 ↔ a < c