Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda.....