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