proposition: Lemma exists_inb D P (x : T) : D x -> P x -> [exists (x | D x), P x].
proof: Proof. by move=> Dx Px; apply/exists_inP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)