law nat_mod_mul_add

lawful-words@0.1.0.0 · LAWS.bend:571

import Base

571law nat_mod_mul_add:
572  for q: Nat
573  for b: Nat
574  for r: Nat
575  for h: {Nat.is_lt(r, b) == True{} : Bool}
576  {Nat.mod(Nat.add(Nat.mul(q, b), r), b) == r : Nat}