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