  We deal with the distribution of N points placed consecutively around the
circle by a fixed angle of a. From the proof of Tony van Ravenstein, we propose
a detailed proof of the Steinhaus conjecture whose result is the following: the
N points partition the circle into gaps of at most three different lengths. We
study the mathematical notions required for the proof of this theorem revealed
during a formal proof carried out in Coq.
