proposition: Lemma imageP A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A).
proof: Proof. by apply: (iffP mapP) => [] [x Ax y_fx]; exists x; rewrite // mem_enum in Ax *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)