proposition: Lemma sup_mono (s1 s2 : Pred T) : s1 <=p s2 -> sup s1 <== sup s2.
proof: Proof. by move=>H; apply: supM=>y; move/H; apply: supP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)