ProofNum.qg1: law of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
Lines 92-104 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=92&end_line=104

import Base

law qg1:
  for +N1: Nat
  for +Qn: Nat
  for +R: Nat
  for +T: 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 +eN: {N1 == Nat.sub(M, 1n) : Nat}
  {Nat.add(Nat.mul(Qn, 10n), 5n) == Nat.sub(M, 1n) : Nat}

Uses (7):
  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.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