proposition: Lemma domf_reduce f : domf (reducef f) = [fsetval x : domf f | f x].
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)