proposition: Lemma existsPP : reflect (exists x, PP x) [exists x, P x].
proof: Proof. by apply: (iffP pred0Pn) => -[x /viewP]; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)