proposition: Lemma fnd_fcat k s1 s2 : fnd k (fcat s1 s2) = if k \in supp s2 then fnd k s2 else fnd k s1.
proof: Proof. elim/fmap_ind': s2 k s1=>[|k2 v2 s2 H IH] k1 s1. - by rewrite fcats0. rewrite supp_ins inE /=; case: ifP; last first. - move/negbT; rewrite negb_or; case/andP=>H1 H2. by rewrite fcat_sins fnd_ins (negbTE H1) IH (negbTE H2). case/orP; first by move/eqP=><-; rewrite fcat_sins !fnd_ins eq_refl. move=>H1; rewrite fcat_sins !fnd_ins. by case: ifP=>//; rewrite IH H1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)