gowers_pb

A small Coq proof for an exercise that was probably taken from the mathematical olympiads