  Consider the puzzle: given a number, remove $k$ digits such that the
resulting number is as large as possible. Various techniques were employed to
derive a linear-time solution to the puzzle: predicate logic was used to
justify the structure of a greedy algorithm, a dependently-typed proof
assistant was used to give a constructive proof of the greedy condition, and
equational reasoning was used to calculate the greedy step as well as the
final, linear-time optimisation.
