solveSquare

write a function that, given natural number t, find the minimum n such that n*n>=t.

Function Signature

def solveSquare(t:Nat): Nat

Theorem Signature

theorem solveSquare_isgeq(t:Nat): (solveSquare t)*(solveSquare t)>=t

Additional Theorem Signature

theorem solveSquare_ismin(t:Nat): Not (∃ y< (solveSquare t), y*y>=t)

View All Submissions

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