proposition: Lemma bij_on_image A (x0 : T) : {on [pred y in image f A], bijective f}.
proof: Proof. exact: subon_bij (@image_codom A) (bij_on_codom x0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)