proposition: Lemma algR_ler_norm_add x y : algR_norm (x + y) <= (algR_norm x + algR_norm y).
proof: Proof. exact: ler_norm_add. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)