Natural numbers - Implementation (more functions) : Use_nat

let rec add = function

  m, n -> if is_zero (n)

            then m

            else if is_even_non_zero (n)

                   then add (add (m, inv_d0 (n)), inv_d0 (n))

                   else (* is_odd (n) *)

                        suc (add (add (m, inv_d1 (n)), inv_d1 (n)))