A three step induction proof

Define a function div3 which maps every n:nat to the integer part of n/3. Show that div3 n is less or equal than n.

Solution

Look at This file