π with Leftovers: A Mechanisation in Agda. - Uma Zalakain; Ornela Dardha (FORTE, 2021)