proposition: Lemma algR_ler_def (x y : algR) : (x <= y) = (algR_norm (y - x) == y - x).
proof: Proof. by apply: ler_def. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)