proposition: Lemma mproperEneq A B : A `<` B = (A != B) && (A `<=` B).
proof: Proof. by rewrite andbC eqEmsubset negb_and andb_orr andbN. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap