proposition: Lemma num_abs_eq0 a : (`|a|%:nng == 0%:nng) = (a == 0).
proof: Proof. by rewrite -normr_eq0. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)