Commit 2026-04-17 12:17 5ed069f9

chore: make argument in bddAbove_of_small implicit (#37648) We use the theorem with an implicit argument much more (~80 times) than we use it with an explicit one (twice). We also deprecate the redundant bddAbove_range lemmas.