Natural numbers - Implementation (more functions) : Use_nat_2.two

let rec two_times = function

  n -> if is_zero (n)

         then zero ()

         else if is_one (n)

                then sucsuc (zero ())

                else sucsuc (sucsuc (two_times (prepre (n))))