proposition: Lemma image_iinv A y (fTy : y \in codom f) : (y \in image f A) = (iinv fTy \in A).
proof: Proof. by rewrite -mem_image ?f_iinv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)