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.
Edited by Paolo G. Giarrusso
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.