When using the Norm module in unstable.v, lemmas for seminorms and norms as defined in this module, and lemmas for |_| as defined in numerical for mathcomp are in conflict. This is due to the fact that |_| does not inherit from the norm structure and should be solved when the Norm module is properly ported to mathcomp.
Moreover, naming is not coherent. One must use Num.Theory.ler_normD for using ler_normD on || (by default it applies to a seminorm) but Norm.Theory.normN to use normN on a seminorm (it applies by default to ||).
When using the Norm module in
unstable.v, lemmas for seminorms and norms as defined in this module, and lemmas for|_|as defined in numerical for mathcomp are in conflict. This is due to the fact that|_|does not inherit from the norm structure and should be solved when the Norm module is properly ported to mathcomp.Moreover, naming is not coherent. One must use
Num.Theory.ler_normDfor usingler_normDon || (by default it applies to a seminorm) butNorm.Theory.normNto usenormNon a seminorm (it applies by default to ||).