proposition: Lemma dinjectiveP D : reflect {in D &, injective f} (dinjectiveb D).
proof: Proof. rewrite -[dinjectiveb D]negbK. case: dinjectivePn=> [noinjf | injf]; constructor. case: noinjf => x Dx [y /andP[neqxy /= Dy] eqfxy] injf. by case/eqP: neqxy; apply: injf. move=> x y Dx Dy /= eqfxy; apply/eqP; apply/idPn=> nxy; case: injf. by exists x => //; exists y => //=; rewrite inE /= eq_sym nxy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)