proposition: Lemma lim_liftE (D : cpo) (s : chain D) : lim s = lim (lift_chain s).
proof: Proof. apply: poset_asym; apply: limM=>y H; first by apply: limP; right. by case: H; [move=>-> | apply: limP]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)