proposition: Lemma rsum_freeon1 n2 (d : 'rV['F_2]_n) (F : 'rV_n -> R) : \sum_(t = d [~[set n2]]) F t = (F (d `[ n2 := Zp0 ]) + F (d `[ n2 := Zp1 ]))%R.
proof: Proof. transitivity (\sum_(t | (t \in [set d `[ n2 := x ] | x in 'F_2])) F t)%R. apply eq_bigl => /= t. by rewrite freeon1. rewrite big_imset /=; last by exact: inj_row_set. rewrite (bigID (pred1 Zp0)) /= (big_pred1 Zp0) //. rewrite (bigID (pred1 Zp1)) /= (big_pred1 Zp1); last by case/F2P. rewrite big_pred0; last by case/F2P. by rewrite addR0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2