proposition: Lemma total_algR : total (<=%O : rel (algR : porderType _)).
proof: Proof. by move=> x y; apply/real_leVge/valP/valP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)