proposition: Lemma restrictf_cat_domr f g : (f + g).[& domf g] = g.
proof: Proof. rewrite catfE restrictf_cat restrictf_comp. by rewrite fsetIDAC fsetDIl fsetDv fsetI0 restrictf0 restrictfT cat0f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)