mathlib3

023a7838 - feat(logic/nontrivial): `exists_pair_lt` (#12925)