proposition: Lemma fcat_rems k s1 s2 : k \notin supp s2 -> fcat (rem k s1) s2 = rem k (fcat s1 s2).
proof: Proof. elim/fmap_ind': s2 k s1=>[|k2 v2 s2 H IH] k1 v1. - by rewrite !fcats0. rewrite supp_ins inE /= negb_or; case/andP=>H1 H2. by rewrite fcat_sins IH // ins_rem eq_sym (negbTE H1) -fcat_sins. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)