Remove `bigmaxr` from `Rstruct.v`?

[affeldt-aist]

analysis/reals_stdlib/Rstruct.v

Line 551 in 3b30884

Definition bigmaxr (r : R) s := \big[Num.max/head r s]_(i <- s) i.

as discussed in the conversation of PR #1736

@t6s @CohenCyril

[CohenCyril]

What is the candidate replacement for this bigmaxr?

[affeldt-aist]

The bigmax offered by order.v.

[CohenCyril]

Ok, then it's not 100% clear for that the bigmaxr can actually be subsumed without overhead (because of head x r in its definition), I think one needs to try and see.

[affeldt-aist]

Yes, indeed. That's why we kept it for a while with a deprecation comment inviting to look at order.v. The full story is that with @drouhling we actually tried both approaches and concluded (iirc) that the one with head x r was harder to use. But that was a long time ago, maybe it's time to let it go? :-(

[affeldt-aist]

Related to issue #2093