Sqrtn.iter_sq: 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 74-85 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=74&end_line=85

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend as RT

def iter_sq(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}, +hf: {Nat.is_le(g, fuel) == True{} : Bool}) -> {Nat.is_le(Nat.mul(M.sqrt_iter(fuel, n, g, m, down), M.sqrt_iter(fuel, n, g, m, down)), n) == True{} : Bool}:
  match fuel down:
    case 0n False{}:
      %Equal.sym(Nat, g, 0n, le_zero(g, hf)) : {Nat.is_le(Nat.mul(_, _), n) == True{} : Bool}
      N.zero_le(n)
    case 0n True{}:
      %Equal.sym(Nat, g, 0n, le_zero(g, hf)) : {Nat.is_le(Nat.mul(_, _), n) == True{} : Bool}
      N.zero_le(n)
    case 1n+f False{}:
      stop_sq(n, g, Equal.trans(Bool, Nat.is_lt(M.sqrt_next(n, g), g), Nat.is_lt(m, g), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, g), M.sqrt_next(n, g), m, Equal.sym(Nat, m, M.sqrt_next(n, g), hm)), Equal.sym(Bool, False{}, Nat.is_lt(m, g), hd)))
    case 1n+ +f True{}:
      iter_sq(f, n, m, M.sqrt_next(n, m), Nat.is_lt(M.sqrt_next(n, m), m), {==}, {==}, RT.shrink(m, g, f, Equal.sym(Bool, True{}, Nat.is_lt(m, g), hd), hf))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_le
  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/lib/nat.bend&name=zero_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend&name=shrink
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend&name=le_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend&name=stop_sq
  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