fact: Definition pair_sup (s : Pred tp) : tp := (sup [Pred p | exists f, p = f.1 /\ f \In s], sup [Pred p | exists f, p = f.2 /\ f \In s]).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)