proposition: Lemma contE (s : chain D1) (C : continuous) : f (lim s) = lim [f ^^ s by cont_mono C].
proof: Proof. case: C=>M E; rewrite E; congr (lim (image_chain _ _)). apply: proof_irrelevance. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype) LemmaOverloading(rels prelude)