tentative definition of bigmaxr with bigop

[affeldt-aist]

rfc

[drouhling]

Another experiment with bigop and maxr is in the bigmaxr branch.

[drouhling]

I'll merge bigmaxr in entourages, since it is sufficient for the purpose of #112.

However it would be nice to extend it with something similar to bigmaxr_mem (replacing head r s with any default value x smaller than all the elements of the family), maybe reusing parts of your work. But this should not be in Rstruct.v, since this has nothing to do with R.

[affeldt-aist]

A replacement for bigmaxr_mem (as mentioned by @drouhling ) has already been merged into master (in normedtype.v). The commit of this PR is about Rstruct.v, at a time when we were still relying on it. We can forget about it. We can also merge it to keep Rstruct.v as up-to-date as possible (I know at least one project that is using Rstruct.v through mathcomp-analysis).