proposition: Lemma emptyset_least E: least (subp_order E) emptyset.
proof: Proof. have eP := (setP_0i E). move/sub_set0:(setI_s1 eP) => h. by rewrite -h;apply: setI_least; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)