coq - Coq ss 反映总和的总和

Question

我一直在寻找一个ssreflect表示总和线性的引理，以便我可以转换

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

进入

sum(a+b) =sum(c)

然后导出为

a+b = c.

在这种情况下哪个可能合适？

目标：

\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

Answer 1

我认为您正在寻找big_split引理。但是如果不知道您要更详细地证明什么目标，就很难知道...