proposition: Lemma chain_closI (s1 s2 : Pred T) : chain_closed s1 -> chain_closed s2 -> chain_closed (PredI s1 s2).
proof: Proof. move=>[H1 S1][H2 S2]; split=>// d H. by split; [apply: S1 | apply: S2]=>// x; case/H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)