law mul_mod_right_sym

bend-mathlib@0.8.1.0 · nat.bend:4444

import Base

4444# A multiple of a leaves no remainder modulo a: (a * b) % a = 0, reversed to rewrite toward the simple side.
4445law mul_mod_right_sym:
4446  for a: Nat
4447  for b: Nat
4448  {0n == Nat.mod(Nat.mul(a, b), a) : Nat}