consider using mathcomp structures to define altMonad and altCIMonad

[t6s]

Following the pattern in convexMonad/probMonad, altMonad and altCIMonad can be defined
using the semigroup and join-semilattice classes from mathcomp.
This would clarify the theory and probably leads to less explicit coercions in proofs.