proposition: Lemma ideal_supP (s : Pred (ideal P)) p : p \In s -> p <== ideal_sup s.
proof: Proof. by move=>H; apply: supP; exists p. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)