Euclidean division by 2

Define a recursive function restecting the following specification:

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

Remark

We all know that there exists in Coq's standard library such a function for euclidean division by any positive integer, but we just ask for a simpler development.

Solution

Look at This file