#lang ivy1.6

type t
interpret t->int

function sumdiv(N:t,X:t):t

definition sumdiv(N,X) = 0 if X <= 0 else (X/N + sumdiv(N,X-1))
proof rec[t]