In response only to the third point, there are some very nice examples of "advanced" equational reasoning in the work of Richard Bird. Pearls of Functional Algorithm Design [0] is a great book for exploring this and demonstrates a very "expert" nature.

[0]: https://www.amazon.com/Pearls-Functional-Algorithm-Design-Ri...