proposition: Lemma finsupp_with f x y : finsupp [fsfun f with x |-> y] = if y == default x then finsupp f `\ x else x |` finsupp f.
proof: Proof. apply/fsetP=> z; rewrite mem_finsupp fsfun_withE (fun_if (fun p => z \in p)). rewrite (fun_if (fun t => t != _)) -mem_finsupp !inE. by case: (altP (z =P x)) => [->|_]; case: (altP (y =P _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)