proposition: Lemma ideal_supM (s : Pred (ideal P)) p : (forall q, q \In s -> q <== p) -> ideal_sup s <== p.
proof: Proof. by move=>H; apply: supM=>y [q][H1] <-; apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)