proposition: Lemma properEneq A B : A \proper B = (A != B) && (A \subset B).
proof: Proof. by rewrite andbC eqEsubset negb_and andb_orr andbN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)