This, I will explain, is not a duplicate of this I think because it has 2 parts and because I have some things to add on to it.
There are 2 questions:
Specifically, I do not get (for the first part) why every group of odd order is solvable implies that the only simple groups of odd order are those of prime order. In the comments, what does it mean that "Solvable groups can either be prime cyclic or non-simple because by definition, solvable groups are extension of prime cyclic groups"? I know the precise definition of a solvable group but I do not understand this statement or how it plays part in the proof. If you could provide a detailed answer to (1) that'd be great.
For the second part, what exactly did Gonthier and his colleagues add to the original proof of Feit-Thompson? If it were really just formalizing bunch of 'intuitive' statements and computer-checking things, why did it take so much time, and why is Feit-Thompson's original proof in the mid-1900s still considered valid even if it had significant holes that Gonthier and his colleagues filled in? I am not looking for a generalized answer for this one, or an analogy, but someone who is quite knowlegeable about this theorem's proof.
If there is no answer for part (2), I will take an aswer to only (1) after 1-3 weeks.