proposition: Lemma supp_fcat s1 s2 : supp (fcat s1 s2) =i [predU supp s1 & supp s2].
proof: Proof. elim/fmap_ind': s2 s1=>[|k v s L IH] s1. - by rewrite supp_nil fcats0 => x; rewrite inE /= orbF. rewrite fcat_sins ?notin_path // => x. rewrite supp_ins !inE /=. case E: (x == k)=>/=. - rewrite ?inE !supp_ins ?inE E orbT. reflexivity. rewrite ?inE. rewrite ?supp_ins. rewrite ?inE /=. rewrite IH. rewrite ?inE /=. rewrite E /=. reflexivity. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)