proposition: Lemma sup_closP (s : Pred T) : sup_closed (sup_closure s).
proof: Proof. split; first by move=>t _ []. move=>d H1 t H3 H4; move: (sup_clos_min H3 H4)=>{H3} -H3. by case: H4=>_; apply=>// x; move/H1; move/H3. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)