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