Refactor monalg.v

- rename `m_scope` to `monom_scope`,
- rename some definitions to follow the naming convention of MathComp, e.g.,
  `cmone` -> `onecm`,
- remove the `{finsfun K -> T / x}` notation (use `{fsfun K -> T with x}`
  instead),
- remove the `malg_val` coercion since it is confusing,
- turns `malgC` from a definition into a notation and some lemmas about `malgC`
  are subsumed by ones about `mkmalgU`.