solveGeom

write a function that, given natural numbers a and t, with a>1, find the minimum n such that a^0+a^1+..a^n >=t.

Function Signature

def solveGeom(a t:Nat)(h:a>1):Nat

Theorem Signature

theorem solveGeom_isgeq(a t:Nat)(h:a>1): a^((solveGeom a t h)+1)-1 >=t*(a-1)

Additional Theorem Signature

theorem solveGeom_ismin(a t:Nat)(h:a>1): Not (∃ y<solveGeom a t h, a^(y+1)-1>= t*(a-1))

View All Submissions

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