我正在尝试学习 Agda。任何人都可以完成这个证明（如果它在正确的轨道上）或指向我现有的文章？我进行了广泛的搜索。
sum : ? ? ?
sum 0 = 0
sum (suc a) = (suc a) + sum a
prove2*Sumn=n*sucn : (n : ?) ? ((sum n) * 2) ? (n * (suc n))
prove2*Sumn=n*sucn zero = refl
prove2*Sumn=n*sucn (suc a) = {! !}