proposition: Lemma reducef_subproof f (x : [fsetval x : domf f | f x]) : f (fincl (fset_sub_val _ _) x).
proof: Proof. set y := (y in f y); suff : val y \in [fsetval x : domf f | f x]. by rewrite val_in_fset. by suff -> : val y = val x by exact: valP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)