proposition: Lemma tuto_forallP : reflect (forall x, P x) [forall x, P x].
proof: Proof. by apply: (iffP pred0P) => P_ x /=; rewrite ?P_ ?(negbFE (P_ x)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)