proposition: Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x].
proof: Proof. by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)