Good post. But it also shows, in a way, what a tangled web Lean is when you get into it! Sure, you could try to just program in Lean, but that would be a shame - proof is such an inherent part of the whole outlook, but proof brings you into a new viewpoint few programmers have. Perhaps Lean needs a hypertext where pathways follow what the reader needs, with the ability to back up and follow another path, rather than needing to have so many books open in separate tabs.