NatDivision.quotient_remainder: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_division.bend as NatDivision
Lines 95-101 of stelliferous@0.0.2.0/proofs/nat_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&start_line=95&end_line=101

import Base

law quotient_remainder:
  for +q: Nat
  for +r: Nat
  for +b: Nat
  for +positive: {Nat.is_lt(0n,b) == True{} : Bool}
  for +bounded: {Nat.is_lt(r,b) == True{} : Bool}
  {Nat.divmod(Nat.add(Nat.mul(q,b),r),b) == (q,r) : Nat & Nat}

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.divmod
  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=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=add_divisor
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=bump
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=small
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=associative