proposition: Lemma fcat_srem k s1 s2 : k \notin supp s1 -> fcat s1 (rem k s2) = rem k (fcat s1 s2).
proof: Proof. elim/fmap_ind': s2 k s1=>[|k2 v2 s2 H IH] k1 s1. - rewrite rem_empty fcats0. elim/fmap_ind': s1=>[|k3 v3 s3 H1 IH]; first by rewrite rem_empty. rewrite supp_ins inE /= negb_or. case/andP=>H2; move/IH=>E; rewrite {1}E . by rewrite ins_rem eq_sym (negbTE H2). move=>H1; rewrite fcat_sins rem_ins; case: ifP=>E. - by rewrite rem_ins E IH. by rewrite rem_ins E -IH // -fcat_sins. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)