proposition: Lemma ler_nnorml v x : x < 0 -> `|v| <= x = false.
proof: Proof. by move=> h; rewrite lt_geF //; apply/(lt_le_trans h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)