proposition: Lemma pair_limM (s : chain tp) x : (forall y, y \In s -> y <== x) -> pair_lim s <== x.
proof: Proof. by split; apply: limM=>y [z][->]; case/H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)