def iter_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/sqrtn.bend:123

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

123def 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}:
124  match fuel down:
125    case 0n False{}:
126      hn
127    case 0n True{}:
128      hn
129    case 1n+f False{}:
130      hn
131    case 1n+ +f True{}:
132      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)))