proposition: Lemma subEfproper A B : A `<=` B = (A == B) || (A `<` B).
proof: Proof. by rewrite eqEfsubset -andb_orr orbN andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)