proposition: Lemma exists_inPP D P PP : (forall x, reflect (PP x) (P x)) -> reflect (exists2 x, D x & PP x) [exists (x | D x), P x].
proof: Proof. by move=> vP; apply: (iffP (exists_inP _ _)) => -[x?/vP]; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)