ProofNum.QG: law of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
Lines 113-129 of lawful-fields@0.1.1.0/proof_num.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_num.bend&start_line=113&end_line=129

import Base

# M = 10 q + 6, from 2^32 - 1 = 10 q + 5 with every number abstract.
law QG:
  for +N1: Nat
  for +Qn: Nat
  for +R: Nat
  for +T: Nat
  for +Z: Nat
  for +M: Nat
  for +hdm: {Nat.add(Nat.mul(Nat.div(N1, T), T), Nat.mod(N1, T)) == N1 : Nat}
  for +hd: {Nat.div(N1, T) == Qn : Nat}
  for +hr: {Nat.mod(N1, T) == R : Nat}
  for +hT: {T == 10n : Nat}
  for +hR: {R == 5n : Nat}
  for +hZ: {Z == 0n : Nat}
  for +hN: {N1 == Nat.sub(Nat.sub(M, 1n), Z) : Nat}
  for +hM: {Nat.is_lt(0n, M) == True{} : Bool}
  {Nat.add(Nat.mul(Qn, 10n), 6n) == M : Nat}

Uses (15):
  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_lt
  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=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=qg1
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=succ_pred
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=sub_zero