proposition: Lemma remf_comp f A B : f.[\ A].[\ B] = f.[\ A `|` B].
proof: Proof. by apply/fmapP=> k; rewrite !fnd_rem inE; do !case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)