Ssreflect Users Discussion List

[bertot <>]

On 11/4/12 3:52 PM, Thomas Sibut-Pinote wrote:
> Hi,
> I've noticed that one cannot use big_nat_recr when there is a non 
> trivial predicate in a sum. How does one separate the last term from 
> the whole sum in such a case?
> Thanks for your time,
> Thomas
You can use another theorem to replace the non-trivial predicate with a 
trivial one, replacing the values being summed by values conditioned by 
this predicate.  See the theorem:big_mkcond

Yves