https://math-comp.github.io/mcb/
https://www.labri.fr/perso/casteran/CoqArt/

2013
https://homepage.mi-ras.ru/~sk/lehre/coq/coq_pract.pdf