Derivatives of real functions defined on proper closed intervals (#1680)

Completes #1615 .  Builds on #1679.

We don't show any of the handy laws of derivatives yet, but show that
differentiability is a proposition.

Author: lowasser

src/analysis.lagda.md

@@ -4,6 +4,7 @@
 module analysis where
 
 open import analysis.convergent-series-metric-abelian-groups public
+open import analysis.derivatives-of-real-functions-on-proper-closed-intervals public
 open import analysis.metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public
 ```