proposition: Lemma disjoint_catfAC f g h : [disjoint domf g & domf h]%fmap -> f + g + h = f + h + g.
proof: Proof. by move=> dgh; rewrite catfAC remf_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)