proposition: Lemma chain_clos_diag (T : cpo) (s : Pred (T * T)) : chain_closed s -> chain_closed [Pred t : T | (t, t) \In s].
proof: Proof. move=>[B H1]; split=>// d H2. rewrite InE /= -{1}(proj1_diagE d) -{2}(proj2_diagE d). by apply: H1; case=>x1 x2 [x][[<- <-]]; apply: H2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)