Induction should now be correct. Added lemmas needed for the induction steps, such as the product of two normal subgroups being a normal subgroup...