Sqrtn.iter_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend as Sqrtn
Lines 123-132 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend&start_line=123&end_line=132

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

def iter_lt(fuel: Nat, +n: Nat, +g: Nat, +m: Nat, +down: Bool, +hm: {m == M.sqrt_next(n, g) : Nat}, +hd: {down == Nat.is_lt(m, g) : Bool}, +hn: {Nat.is_lt(n, Nat.mul(1n+g, 1n+g)) == True{} : Bool}) -> {Nat.is_lt(n, Nat.mul(1n+M.sqrt_iter(fuel, n, g, m, down), 1n+M.sqrt_iter(fuel, n, g, m, down))) == True{} : Bool}:
  match fuel down:
    case 0n False{}:
      hn
    case 0n True{}:
      hn
    case 1n+f False{}:
      hn
    case 1n+ +f True{}:
      iter_lt(f, n, m, M.sqrt_next(n, m), Nat.is_lt(M.sqrt_next(n, m), m), {==}, {==}, step_any(n, g, m, hm, Equal.sym(Bool, True{}, Nat.is_lt(m, g), hd)))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend&name=step_any
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=sqrt_iter
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=sqrt_next