Ordinals#545

finegeometer wants to merge 2 commits intothe1lab:mainthe1lab/1lab:mainfrom

finegeometer:ordinalsfinegeometer/1lab:ordinalsCopy head branch name to clipboard