let rec pre = function
n -> if is_odd (n)
then
if is_zero (inv_d1 (n))
then zero ()
else d0 (inv_d1 (n))
else
if is_even_non_zero (n)
then d1 (pre (inv_d0 (n)))
else failwith ("pre : requires a non-zero natural number as its argument")