Computing Persistent Homology within Coq/SSReflect | Publicación