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 _ _)). by apply: pf_irr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)