coqproofcoq-tacticssreflect

Coq ssreflect sum of sums

I have been searching for a lemma in ssreflect that represents sum linearity, so that I could transform

sum(a) + sum(b) = sum(c)

into

sum(a+b) =sum(c)

and then derive into

a+b = c.

Which could be suitable in this case?

The goal:

\big[Rplus/0]_(i <- fin_img (A:=U) (B:=R_eqType) X) (.  .  .) +
\big[Rplus/0]_(i <- fin_img (A:=U) (B:=R_eqType) X) (.  .  .) =
\sum_(u in U) X u * `p_ X u
Solution

  • I think you are looking for the big_split lemma. But it is hard to know without knowing what goal you're trying to prove in more detail...