proposition: Lemma image_codom A : {subset image f A <= codom f}.
proof: Proof. by move=> _ /imageP[x _ ->]; apply: codom_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)