proposition: Lemma rsum_freeon0 (d : 'rV['F_2]_n) (F : 'rV_n -> R) : \sum_(t = d [~set0]) F t = F d.
proof: Proof. transitivity (\sum_(t | t == d) F t)%R. apply eq_bigl => /= t; by rewrite freeon0 eq_sym. by rewrite (big_pred1 d). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2