finish Induction.v except part c of 5 star exercise; unable to finish that for now