proposition: Lemma sol_der1_proper G H : solvable G -> H \subset G -> H :!=: 1 -> H^`(1) \proper H.
proof: Proof. move=> solG sHG ntH; rewrite properE comm_subG //; apply: implyP ntH. by have:= forallP solG H; rewrite subsetI sHG implybNN. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)