proposition: Lemma supportP y D g : reflect (forall x, x \notin D -> g x = y) (y.-support g \subset D).
proof: Proof. by apply: (iffP subsetP) => Dg x; [apply: contraNeq | apply: contraR] => /Dg->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)