People, is there publicly available a proof in Agda of the Ramsey's theorem (about the size of a monochromatic sub-graph in a complete graph) ? Thanks, ------ Sergei