proposition: Lemma norm_snum_subproof {V : normedZmodType R} (x : V) : Signed.spec 0 ?=0 >=0 `|x|.
proof: Proof. by rewrite /=. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)