Peano arithmetic in C++ type system

peano.h

#include <type_traits>

// Natural numbers
struct nat { };

// Typed only if T is derived from nat
template <typename T>
using nat_only = std::enable_if_t<std::is_base_of<nat, T>::value>;

// Zero is a natural number
struct zero : nat { };

// So is the successor of a natural number
template <typename T, typename = nat_only<T>>
struct succ : nat { };

// A few numbers...
using one = succ<zero>;
using two = succ<one>;
using three = succ<two>;
using four = succ<three>;
using five = succ<four>;

// Conversion to int
template <typename T>
struct to_int { };

template <>
struct to_int<zero> { static constexpr int value = 0; };

template <typename Pred>
struct to_int<succ<Pred>> { static constexpr int value = 1 + to_int<Pred>::value; };

// Addition
template <typename X, typename Y, typename = nat_only<Y>>
struct add { };

template <typename Y>
struct add<zero, Y> { using type = Y; };

template <typename Pred, typename Y>
struct add<succ<Pred>, Y> { using type = typename add<Pred, succ<Y>>::type; };

// Assertions
static_assert(0 == to_int<zero>::value, "0 == zero");
static_assert(3 == to_int<three>::value, "3 == three");

static_assert(std::is_same_v<add<two, three>::type, five>, "2 + 3 == 5");
static_assert(std::is_same_v<add<one, four>::type, add<three, two>::type>, "1 + 4 == 3 + 2");