proposition: Lemma imset_set1 x : f @: [set x] = [set f x].
proof: Proof. apply/setP => y. by apply/imsetP/set1P=> [[x' /set1P-> //]| ->]; exists x; rewrite ?set11. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)