fact: Definition ler_normD V (x y : V) : `|x + y| <= `|x| + `|y| := ler_normD x y.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)