Author: Dan Synek
Title: Formalising Lagrange Theorem in Coq
Abstract: 
Lagrange Theorem states that if G is a finite group and H is a subgroup of G,
then the order of H divides the order of G.  It is a nice exercise to
formalise it, since it contains many important notions from algebra, such 
as the formation of quotients and the notion of finiteness. The proof, when
given in normal textbooks, is only a few lines long. The formalised proof
is many pages long. I will try to analyse why, and in particular point out
problems with the use of subsetoids.