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