proposition: Lemma in_iinv_f A : {in A &, injective f} -> forall x fAfx, x \in A -> @iinv A (f x) fAfx = x.
proof: Proof. by move=> injf x fAfx Ax; apply: injf => //; [apply: mem_iinv | apply: f_iinv]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)