Bhavik Mehta: Formalising Sharkovsky's Theorem (Proof Pearl). CPP 2023: 267-274