proposition: Lemma sup_closP (s : Pred T) : sup_closed (sup_closure s).
proof: Proof. split; first by move=>t _ []. move=>d H1 t /sup_clos_min H3 H4. by case: (H4) => _; apply=> x /H1/(H3 H4). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype) LemmaOverloading(rels prelude)