Associativity for scalar mulitiplication operator
The notation "_ :* _" defined here is declared to be left associative. Does it make more sense for it to be right associative? (I am assuming this is the notation for scalar multiplication)
Additionally, to ensure compatibility with mathcomp in the future, could it be possible to add a check in the pipeline that tests if it is possible to import stdpp and ssreflect together?