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