proposition: Lemma finsupp_without f x z : finsupp [fsfun f without x] = finsupp f `\ x.
proof: Proof. by rewrite finsupp_with eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)