remove warnings

- use of MathComp lemmas deprecated since 1.12.0
- relace `ident` by `name` in notations

Author: affeldt-aist

_CoqProject

@@ -10,4 +10,4 @@ set.v
 -arg -w -arg +non-primitive-record
 -arg -w -arg +undeclared-scope
 -arg -w -arg -ambiguous-paths
--arg -w -arg -uniform-inheritance
+-arg -w -arg -uniform-inheritance