sumeN

[affeldt-aist]

Motivation for this change

minor addition, used in the dev of measure theory

Things done/to do

TODO before merge: doppeD, doppeB

• added corresponding entries in CHANGELOG_UNRELEASED.md
  - [ ] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Is it ok if we have adde_def_oppeD and oppeD with fin_num as hypothesis? Same for oppeB.
If it is ok, we can add the versions for doppeD and doppeB and we are done.
There is certainly something more systematic and significant to be done about adde_def
but that can maybe be the purpose of another PR.

[affeldt-aist]

Is it ok if we have adde_def_oppeD and oppeD with fin_num as hypothesis? Same for oppeB. If it is ok, we can add the versions for doppeD and doppeB and we are done. There is certainly something more systematic and significant to be done about adde_def but that can maybe be the purpose of another PR.

"Something more systematic" might go through the introduction of a more generic notation allowing to write
?( x + y). @CohenCyril

I gave it a try with the following reserved notation:

Reserved Notation "'?(' x '+' y ')'" (at level 0, x, y at level 1,
  format "'?(' x  +  y ')'").

One needs then at add parenteses here and there (e.g., ?( (- x) + y))
and it conflicts with SSReflect tactics such as rewrite ?(f x).

There is certainly a better way to declare this notation.

Shall we issue about that and care later?

[CohenCyril]

The question of the notation ?(x + y) is orthogonal, this PR should proceed independently.
(It's ok to introduce and preserve an alias x +? y := ?(x+ y) later on.

However, for this PR, I advocate that the primary lemmas should be the ones with hypothesis x +? y rather than finitude, and hence have oppeD x y : x +? y -> - (x + y) = - x - y.

For the summations, it's the same, the first and primary lemma should be sumeN and use {in P &, forall i j, x i +? x j} instead as usual for summation on general indices.

[CohenCyril]

LGTM