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