什么是重写的最佳方式\sum_(i...) (F i - G i)是(\sum_(i...) F i - \sum_(i...) G i)与序数bigop，假设下溢得到妥善管理？
更准确地说，关于这些下溢，我对以下引理感兴趣：
Lemma big_split_subn (n : nat) (P : 'I_n -> bool) (F G : 'I_n -> nat) :
(forall i : 'I_n, P i -> G i <= F i) ->
\sum_(i < n | P i) (F i - G i) = \sum_(i < n | P i) F i - \sum_(i < n | P i) G i.
似乎big_split …