proposition: Lemma eq_in_imset f g D : {in D, f =1 g} -> f @: D = g @: D.
proof: Proof. move=> eqfg; apply/setP => y. by apply/imsetP/imsetP=> [] [x Dx ->]; exists x; rewrite ?eqfg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)