Arith.le_div_g: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as Arith
Lines 70-80 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&start_line=70&end_line=80

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/proofs/lib/lemmas/proofs/nat_algebra.bend as A

def le_div_g(+x: Nat, +q: Nat, +bp: Nat, +r: Nat, +hr: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.is_le(x, q) == Nat.is_le(Nat.mul(x, 1n+bp), Nat.add(Nat.mul(q, 1n+bp), r)) : Bool}:
  match x q:
    case 0n q0:
      %Equal.sym(Bool, Nat.is_le(0n, q0), True{}, N.zero_le(q0)) : {_ == Nat.is_le(0n, Nat.add(Nat.mul(q0, 1n+bp), r)) : Bool}
      Equal.sym(Bool, Nat.is_le(0n, Nat.add(Nat.mul(q0, 1n+bp), r)), True{}, N.zero_le(Nat.add(Nat.mul(q0, 1n+bp), r)))
    case 1n+ +xp 0n:
      Equal.sym(Bool, Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), r), False{}, N.lt_not_le(r, Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), N.lt_le_trans(r, 1n+bp, Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), hr, N.le_add_right(1n+bp, Nat.mul(xp, 1n+bp)))))
    case 1n+ +xp 1n+ +qp:
      %Equal.sym(Nat, Nat.add(Nat.add(1n+bp, Nat.mul(qp, 1n+bp)), r), Nat.add(1n+bp, Nat.add(Nat.mul(qp, 1n+bp), r)), A.add_assoc(1n+bp, Nat.mul(qp, 1n+bp), r)) : {Nat.is_le(xp, qp) == Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), _) : Bool}
      %Equal.sym(Bool, Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), Nat.add(1n+bp, Nat.add(Nat.mul(qp, 1n+bp), r))), Nat.is_le(Nat.mul(xp, 1n+bp), Nat.add(Nat.mul(qp, 1n+bp), r)), le_add_cancel(1n+bp, Nat.mul(xp, 1n+bp), Nat.add(Nat.mul(qp, 1n+bp), r))) : {Nat.is_le(xp, qp) == _ : Bool}
      le_div_g(xp, qp, bp, r, hr)

Uses (13):
  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.add
  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/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_not_le
  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/arith.bend&name=le_add_cancel