proposition: Lemma algR_normrN x : algR_norm (- x) = algR_norm x.
proof: Proof. by apply/val_inj; apply: normrN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)