proposition: Lemma diag_cont (D : cpo) : continuous (fun x : D => (x, x)).
proof: Proof. exists diag_mono=>d; apply: poset_asym; by split=>/=; [rewrite proj1_diagE | rewrite proj2_diagE]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)