proposition: Lemma wholeset_greatest E: greatest (subp_order E) E.
proof: Proof. have aux: inc E (\Po E) by apply: setP_Ti. have h: union (\Po E) = E. apply:extensionality;last by apply:(setU_s1 aux). by apply:setU_s2 => y /setP_P. by rewrite -{2} h; apply:setU_greatest; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)