proposition: Lemma norm_intr_ge1 x : x \is a int_num -> x != 0 -> 1 <= `|x|.
proof: Proof. rewrite -normr_eq0 => /natr_norm_int/natrP[n ->]. by rewrite pnatr_eq0 ler1n lt0n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)