proposition: Fact eq0_norm x : `|x| = 0 -> x = 0.
proof: Proof. case: (leN_total x) => /ge0_norm => [-> // | Dnx nx0]. by rewrite -[x]opprK -Dnx normN nx0 oppr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)