proposition: Lemma mproper0 A : (mproper mset0 A) = (A != mset0).
proof: Proof. by rewrite /mproper msub0set msubset0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap