Roots.bl_le: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as Roots
Lines 202-210 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend&start_line=202&end_line=210

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/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

# L <= k (1 + L / k)
def bl_le(+kp: Nat, +bl: Nat) -> {Nat.is_le(bl, Nat.mul(1n+kp, 1n+Nat.div(bl, 1n+kp))) == True{} : Bool}:
  +k = {1n+kp : Nat}
  +q = Nat.div(bl, k)
  +r = Nat.mod(bl, k)
  %Equal.sym(Nat, bl, Nat.add(Nat.mul(q, k), r), R.dm_eq(kp, bl)) : {Nat.is_le(_, Nat.mul(k, 1n+q)) == True{} : Bool}
  %Equal.sym(Nat, Nat.mul(k, 1n+q), Nat.add(k, Nat.mul(k, q)), A.mul_succ(k, q)) : {Nat.is_le(Nat.add(Nat.mul(q, k), r), _) == True{} : Bool}
  %Equal.sym(Nat, Nat.add(k, Nat.mul(k, q)), Nat.add(Nat.mul(q, k), k), Equal.trans(Nat, Nat.add(k, Nat.mul(k, q)), Nat.add(Nat.mul(k, q), k), Nat.add(Nat.mul(q, k), k), A.add_comm(k, Nat.mul(k, q)), Equal.cong(Nat, Nat, z => Nat.add(z, k), Nat.mul(k, q), Nat.mul(q, k), A.mul_comm(k, q)))) : {Nat.is_le(Nat.add(Nat.mul(q, k), r), _) == True{} : Bool}
  N.lt_le(Nat.add(Nat.mul(q, k), r), Nat.add(Nat.mul(q, k), k), N.lt_add_left(r, k, Nat.mul(q, k), R.dm_lt(kp, bl)))

Uses (17):
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  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.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt