proposition: Lemma chain_clos_mono (s1 s2 : Pred T) : s1 <=p s2 -> chain_closure s1 <=p chain_closure s2.
proof: Proof. move=>H1; apply: chain_clos_min (chain_closP s2)=>p H2. by apply: chain_clos_sub; apply: H1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)