proposition: Lemma sub_supM (u : Pred tp) (x : tp) : (forall y, y \In u -> y <== x) -> sub_sup u <== x.
proof: Proof. by move=>H; apply: supM=>y [z][H1] ->; apply: H H1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)