proposition: Lemma chain_clos_min (s : Pred T) t : s <=p t -> chain_closed t -> chain_closure s <=p t.
proof: Proof. by move=>H1 H2 p; move/(_ _ H1 H2). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)