proposition: Lemma summary_foldE s d e : summary_powerset s d e = summary_fold s d e.
proof: Proof. rewrite /summary_powerset /summary_fold. rewrite {1 2}(set_mem s). move: (enum s) d e (enum_uniq (ssrbool.mem s)). elim => {s} [|n1 s IH] d e Hs /=. rewrite powerset0 big_set1; congr e. apply/rowP => i; by rewrite mxE /= in_set0. rewrite (partition_big_imset (fun s : {set 'I_n} => n1 \in s)). rewrite (_ : [set n1 \in (s0 : {set 'I_n}) | s0 in _] = [set: bool]); last first. apply/setP => x; rewrite !inE /=. apply/imsetP; case: x. - exists [set n1]; last by rewrite in_set1 eqxx. by rewrite powersetE sub1set !inE eqxx. - exists set0; last by rewrite in_set0. by rewrite powersetE sub0set. rewrite (reindex F2_of_bool bijective_F2_of_bool). apply eq_big => [i|i _]; first by rewrite /= !inE. case/andP : Hs => /= Hn1 Hs. rewrite -IH; last by []. rewrite (reindex_onto (fun f => if i then n1 |: f else f) (fun f => f :\ n1)); last first. move=> /= j; rewrite !inE. move/andP=> [] /subsetP Hj. case: i => Hi. by rewrite setD1K // (eqP Hi). by apply/eqP; rewrite eqEsubset subD1set /= subsetD1 (eqP Hi) andbT. apply eq_big=> j; last first. move=> Hi. congr e. apply/rowP => k; rewrite !mxE !inE /=. case/boolP : (k == n1) => Hkn1 /=. rewrite (eqP Hkn1) (negbTE Hn1). case: ifP Hi => [? Hi|? /=]. by rewrite in_setU1 eqxx. by move=> -/andP[/andP[_ /eqP -> _ //]]. case: ifP => //; case: ifP => //. by rewrite in_setU1 (negbTE Hkn1) orFb. case: ifP => [Hi|Hi]. - rewrite /powerset !inE eqxx andbT /=. case/boolP : (j \subset [set i in s]) => Hj. rewrite setU1K ?eqxx ?andbT; last first. apply: contra Hn1; move/subsetP : Hj => /(_ n1). by rewrite inE. apply/subsetP => x /setU1P -[|] Hx. by rewrite Hx 3!inE eqxx. move/subsetP/(_ _ Hx) : Hj. rewrite !inE => ->; by rewrite orbT. case/boolP : ((n1 |: j) :\ n1 == j) => Hn1j; last first. by rewrite andbF. rewrite andbT. apply: contraNF Hj => /subsetP Hj'. apply/subsetP => k Hk. move: Hj' => /(_ k). rewrite in_setU1 Hk orbT => /(_ isT). rewrite !inE => /orP[/eqP kn1 | //]. by move: Hk; rewrite kn1 -(eqP Hn1j) setD11. - rewrite /powerset !inE. case/boolP : (j \subset [set x in s]) => Hj. case/boolP : (n1 \in j) => Hn1j. move/subsetP/(_ _ Hn1j) : Hj. by rewrite !inE (negbTE Hn1). rewrite eqxx andbT. have -> : j :\ n1 = j. apply/setP => k; rewrite !inE. case/boolP : (k == n1) => //= /eqP ->; by rewrite (negbTE Hn1j). rewrite eqxx andbT. apply/subsetP=> k Hk. move/subsetP/(_ _ Hk): Hj. rewrite !inE => ->; by rewrite orbT. case/boolP : (n1 \in j) => Hn1j; first by rewrite /= andbF. have -> : j :\ n1 = j. apply/setP => k; rewrite !inE. case/boolP : (k == n1) => //= /eqP ->; by rewrite (negbTE Hn1j). rewrite !eqxx !andbT. apply/subsetP => Hjs. move/subsetP: Hj; apply => k Hk. move: (Hjs _ Hk). rewrite !inE => /orP[/eqP ?|//]. by subst n1; rewrite Hk in Hn1j. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2