change the notation for tnth from \_ to avoid a conflict with mca

[t6s]

The notation \_ for tnth defined in ssr_ext.v (at level 9) conflicts with the one in classical_sets (at level 10),
blocking uses of mathcomp-analysis at some places, particularly when trying to reboot PR #67 .

This PR replaces it by \__ (one extra underscore) to avoid the conflict.

[t6s]

I also noticed a few lemmas marked in bayes.v to be moved to ssr_ext.v, and did it.

[affeldt-aist]

This is fine with me. Have you considered other notations of less than 3 characters? Maybe !_ could have worked. It looks like array addressing to me, which seems appropriate here. (This could even be proposed at the MathComp level.)

[affeldt-aist]

This is fine with me. Have you considered other notations of less than 3 characters? Maybe !_ could have worked. It looks like array addressing to me, which seems appropriate here. (This could even be proposed at the MathComp level.)

Haskell is using ! for array subscripting by the way.

[t6s]

This is fine with me. Have you considered other notations of less than 3 characters? Maybe !_ could have worked. It looks like array addressing to me, which seems appropriate here. (This could even be proposed at the MathComp level.)

No, and I have no particular preference. Which do you really like?

[affeldt-aist]

in the circumstances, !_ looks appropriate

[t6s]

looks pretty enough

[affeldt-aist]

Good improvement.