Euclidean division by 2

Define a simple-step recursive function for the following specification:

 Definition div2_mod2 : 
  forall n:nat, {q:nat & {r:nat | n = 2*q + r /\ r <= 1}}.

Solution

Look at This file