Commit 2024-05-04 21:55 a4b23a6d

View on Github →

feat: a / b ≤ c ↔ a / c ≤ b (#12622)

Estimated changes

added theorem div_le_comm₀
added theorem div_lt_comm₀