Do we have the following simple facts about ko stated somewhere in the library?
Hol Igor / Notes On Ko
ProgressRate
HomepagesHoligor