proposition: Lemma algR_ger_leVge (x y : algR) : z <= x -> z <= y -> (x <= y) || (y <= x).
proof: Proof. exact: ger_leVge. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)