Needs the misplaced Acc_rect_max.
Acc_rect_max
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.