proposition: Lemma supM (s : Pred T) x : (forall y, y \In s -> y <== x) -> sup s <== x.
proof: Proof. by case: T s x=>S [[p]][/= s H1 H2 *]; apply: (H2). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)