Abbreviate an ordinal discrete log “constant” and prove it correct.
Prove lemmas 3, 4 and 5 from Manolios and Vroon.