#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]