proposition: Lemma bij_on_codom (x0 : T) : {on [pred y in codom f], bijective f}.
proof: Proof. pose g y := iinv (valP (insigd (codom_f x0) y)). by exists g => [x fAfx | y fAy]; first apply: injf; rewrite f_iinv insubdK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)