Computing persistent homology within Coq/SSReflect | Publicación