proposition: Lemma ler0_ge_norm : {in npos &, {mono (@normr _ R) : x y / x <= y >-> x >= y}}.
proof: Proof. move=> x y; rewrite !nposrE => x0 y0. by rewrite !ler0_norm// -subr_ge0 opprK addrC subr_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)