Análisis computable y nociones de continuidad en Coq