countable.v: prove choose_proper

Needs the misplaced 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.