proposition: Lemma big_orE : \big[orb/false]_(i | P i) B i = [exists (i | P i), B i].
proof: Proof. by rewrite big_has_cond; apply/hasP/existsP=> [] [i]; exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)