Commit 2025-01-27 14:51 ace1a064

chore: rename the fact that (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ in a dense order (#20317) I found those lemma names hard to find, especially because they didn't contain _of_dense or didn't contain lt. Moves:

• le_of_forall_le_of_dense → le_of_forall_gt_imp_ge_of_dense
• le_of_forall_ge_of_dense → le_of_forall_lt_imp_le_of_dense
• forall_lt_le_iff → forall_lt_imp_le_iff_le_of_dense
• forall_gt_ge_iff → forall_gt_imp_ge_iff_le_of_dense
• eq_of_le_of_forall_le_of_dense → eq_of_le_of_forall_lt_imp_le_of_dense
• eq_of_le_of_forall_ge_of_dense → eq_of_le_of_forall_gt_imp_ge_of_dense