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