solveProg

write a function that, given natural number t, find the minimum n such that 1+2+…+n>=t.

Function Signature

def solveProg(t:Nat):Nat

Theorem Signature

theorem solveProg_isgeq(t:Nat): (solveProg t)*((solveProg t)+1) >= t*2

Additional Theorem Signature

theorem solveProg_ismin(t:Nat): Not (∃ y< (solveProg t), y*(y+1)>=t*2)

View All Submissions

Please log in or register to submit a solution for this challenge.