proposition: Lemma big_andE : \big[andb/true]_(i | P i) B i = [forall (i | P i), B i].
proof: Proof. rewrite big_all_cond; apply/allP/forallP=> /= allB i; rewrite allB //. exact: mem_index_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)