ProofFastW2.rg: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_w2.bend as ProofFastW2
Lines 190-201 of lawful-bytes@0.1.1.0/proof_fast_w2.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_w2.bend&start_line=190&end_line=201

import Base
import lawful-words@0.1.0.0/defs.bend as W

# rep(c) == pack4(c, c, c, c), as numbers with 2^32, 2^8, 2^16, 2^24 abstract.
law rg:
  for +c: U32
  for +M: Nat
  for +A: Nat
  for +B: Nat
  for +E: Nat
  for +h1: {U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))) == Nat.mod(Nat.mul(U32.to_nat(c), U32.to_nat(W.pack4(1, 1, 1, 1))), M) : Nat}
  for +h2: {U32.to_nat(W.pack4(1, 1, 1, 1)) == Nat.add(U32.to_nat(1), Nat.add(Nat.mul(U32.to_nat(1), A), Nat.add(Nat.mul(U32.to_nat(1), B), Nat.mul(U32.to_nat(1), E)))) : Nat}
  for +h3: {U32.to_nat(W.pack4(c, c, c, c)) == Nat.add(U32.to_nat(c), Nat.add(Nat.mul(U32.to_nat(c), A), Nat.add(Nat.mul(U32.to_nat(c), B), Nat.mul(U32.to_nat(c), E)))) : Nat}
  for +h4: {Nat.is_lt(U32.to_nat(W.pack4(c, c, c, c)), M) == True{} : Bool}
  {U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))) == U32.to_nat(W.pack4(c, c, c, c)) : 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.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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_w2.bend&name=nk
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=pack4
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mod_small