You need to sign in or sign up before continuing.
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