proposition: Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x].
proof: Proof. exact: 'forall_implyP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)