proposition: Lemma bigjoinPcond r : bigjoin_cond_spec r (\join_(i <- r | P i) F i).
proof: Proof. rewrite -big_filter; case: bigjoinP => [nilPr|i]. by constructor; rewrite all_predC has_filter negbK; case: filter nilPr. by rewrite mem_filter => /andP[? ?]; constructor. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)