proposition: Lemma const_cont (D1 D2 : cpo) (y : D2) : continuous (fun x : D1 => y).
proof: Proof. exists const_mono; move=>s; apply: poset_asym. - by apply: limP; case: s=>[p][[d H1] H2]; exists d. by apply: limM=>_ [x][->]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)