def stop_sq

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

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

55def stop_sq(+n: Nat, +g: Nat, +h: {Nat.is_lt(M.sqrt_next(n, g), g) == False{} : Bool}) -> {Nat.is_le(Nat.mul(g, g), n) == True{} : Bool}:
56  match g:
57    case 0n:
58      N.zero_le(n)
59    case 1n+ +gp:
60      +q = Nat.div(n, 1n+gp)
61      +hge = N.not_lt_le(M.sqrt_next(n, 1n+gp), 1n+gp, h)
62      +h2 = Equal.trans(Bool, Nat.is_le(1n+gp, q), Nat.is_le(Nat.add(1n+gp, 1n+gp), Nat.add(1n+gp, q)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(1n+gp, 1n+gp), Nat.add(1n+gp, q)), Nat.is_le(1n+gp, q), R.le_add_cancel(1n+gp, 1n+gp, q)),
63        Equal.trans(Bool, Nat.is_le(Nat.add(1n+gp, 1n+gp), Nat.add(1n+gp, q)), Nat.is_le(Nat.mul(1n+gp, 2n), Nat.add(1n+gp, q)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(1n+gp, q)), Nat.add(1n+gp, 1n+gp), Nat.mul(1n+gp, 2n), Equal.sym(Nat, Nat.mul(1n+gp, 2n), Nat.add(1n+gp, 1n+gp), RT.two_mul(1n+gp))),
64          Equal.trans(Bool, Nat.is_le(Nat.mul(1n+gp, 2n), Nat.add(1n+gp, q)), Nat.is_le(1n+gp, M.sqrt_next(n, 1n+gp)), True{}, Equal.sym(Bool, Nat.is_le(1n+gp, Nat.div(Nat.add(1n+gp, q), 2n)), Nat.is_le(Nat.mul(1n+gp, 2n), Nat.add(1n+gp, q)), R.le_div(1n, 1n+gp, Nat.add(1n+gp, q))), hge)))
65      Equal.trans(Bool, Nat.is_le(Nat.mul(1n+gp, 1n+gp), n), Nat.is_le(1n+gp, q), True{}, Equal.sym(Bool, Nat.is_le(1n+gp, Nat.div(n, 1n+gp)), Nat.is_le(Nat.mul(1n+gp, 1n+gp), n), R.le_div(gp, 1n+gp, n)), h2)