proposition: Lemma lim_mono (D : cpo) (s1 s2 : chain D) : s1 <=p s2 -> lim s1 <== lim s2.
proof: Proof. by move=>H; apply: limM=>y; move/H; apply: limP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)