law modmulin

lawful-words@0.1.0.0 · proof_word.bend:694

import Base

694law modmulin:
695  for +x: Nat
696  for +y: Nat
697  for +z: Nat
698  for +m: Nat
699  {Nat.mod(Nat.add(x, Nat.mul(y, Nat.mod(z, m))), m) == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}