proposition: Lemma fnd_cat f g k : (f + g).[? k] = if k \in domf g then g.[? k] else f.[? k].
proof: Proof. case: fndP => //= [kfg|]; rewrite /catf /=. rewrite ffunE /=; case: fsetULVR => [kf|kg]; last by rewrite Some_fnd kg. by rewrite -in_fnd; move: kf; rewrite inE => /andP[/negPf ->]. by rewrite mem_catf => /norP [kNf kNg]; rewrite !not_fnd // if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)