proposition: Lemma msetME A B (u : K * K) : (A `*` B) u = A u.1 * B u.2.
proof: Proof. rewrite !fsfunE inE; case: ifPn => //=. by rewrite negb_and !memNfinsupp => /orP [] /eqP->; rewrite ?muln0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap