Commit 2023-06-08 03:38 1507c181

View on Github →

feat: golf using gcongr throughout the library (#4784) Following on from #4702, another hundred sample uses of the gcongr tactic.

Estimated changes

modified theorem smul_le_smul_of_nonneg
modified theorem smul_lt_smul_of_pos