proposition: Lemma normrN1 : `|-1| = 1 :> R.
proof: Proof. have: `|-1| ^+ 2 == 1 :> R by rewrite expr2 /= -normM mulrNN mul1r -[1]subr0 -le_def le01. rewrite sqrf_eq1 => /predU1P [] //; rewrite -[-1]subr0 -le_def. have ->: 0 <= -1 = (-1 == 0 :> R) || (0 < -1) by rewrite lt_def; case: eqP => // ->; rewrite lerr. by rewrite oppr_eq0 oner_eq0 => /(addr_gt0 lt01); rewrite subrr ltrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)