proposition: Lemma morphim_eq0 A : A \subset D -> (f @* A == set0) = (A == set0).
proof: Proof. by rewrite imset_eq0 => /setIidPr->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)