小编Pie*_*lot的帖子

在 bigop 上分配减法

什么是重写的最佳方式\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 …

coq ssreflect

4
推荐指数
1
解决办法
155
查看次数

标签 统计

coq ×1

ssreflect ×1