proposition: Lemma normrN1 : `|-1 : R| = 1.
proof: Proof. have: `|-1 : R| ^+ 2 == 1 by rewrite -normrX -signr_odd normr1. rewrite sqrf_eq1 => /orP[/eqP //|]; rewrite -ger0_def le0r oppr_eq0 oner_eq0. by move/(addr_gt0 ltr01); rewrite subrr ltxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)