proposition: Lemma chain_clos_idemp (s : Pred T) : chain_closed s -> chain_closure s =p s.
proof: Proof. move=>p; split; last by apply: chain_clos_sub. by apply: chain_clos_min=>//; apply: chain_closP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)