proposition: Lemma codomP y : reflect (exists x, y = f x) (y \in codom f).
proof: Proof. by apply: (iffP (imageP _ y)) => [][x]; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)