proposition: Lemma big_subseqs_cons_cond (F : seq T -> R) (P : pred (seq T)) (a : T) (s : seq T) : uniq (a :: s) -> \big[*%M/1]_(i : subseqs (a :: s) | P i) F i = \big[*%M/1]_(i : subseqs s | P (a :: i)) F (a :: i) * \big[*%M/1]_(i : subseqs s | P i) F (i).
proof: Proof. move=> asuniq. rewrite big_mkcond (big_subseqs_cons (fun i => if P i then F i else 1)) //. by congr (_ * _); rewrite -big_mkcond. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted