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