law mul_mod

lawful-words@0.1.0.0 · proof_nat.bend:1114

import Base

1114law mul_mod:
1115  for +a: Nat
1116  for +b: Nat
1117  {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}