In this thesis we present a formalization of the combinatorial part of the proof of Feit-Higman theorem on generalized polygons. Generalised polygons are abstract geometric structures that generalize ordinary polygons and ...