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