Commit 2025-10-17 14:39 108140a1

View on Github →

chore: use grw, gcongr more (#30508) Golf many proofs using grw, gcongr, cutsat, linarith... For this, tag a few more lemmas with gcongr, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by #30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.

Estimated changes

modified theorem mabs_mul_three
modified theorem kstar_mul_le
modified theorem mul_kstar_le
modified theorem add_le_add_add_tsub
modified theorem Hyperreal.isSt_sSup
modified theorem Nat.count_mono_left
modified theorem Nat.dist_add_add_right
modified theorem Nat.dist_eq_intro
modified theorem Nat.dist_eq_max_sub_min
modified theorem Nat.dist_eq_sub_of_le
modified theorem Nat.dist_eq_zero
modified theorem Nat.dist_pos_of_ne
modified theorem Nat.dist_succ_succ
modified theorem Nat.dist_tri_left'
modified theorem Nat.dist_tri_left
modified theorem Nat.dist_tri_right'
modified theorem Nat.dist_tri_right
modified theorem Nat.dist_zero_left
modified theorem Nat.dist_zero_right
modified theorem Nat.eq_of_dist_eq_zero
modified theorem Poly.sumsq_nonneg
modified theorem edist_triangle4