proposition: Lemma norm_eq0 x : norm x = 0 -> x = 0.
proof: Proof. case: x => x1 x2 /eqP; rewrite eq_le num_le_maxl 2!normr_le0 -andbA/=. by case/and3P => /eqP -> /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect fingroup ssralg poly ssrnum) signed