law mul_mod_right

bend-mathlib@0.8.1.0 · nat.bend:2102

import Base

2102# A multiple of a leaves no remainder modulo a: (a * b) % a = 0.
2103law mul_mod_right:
2104  for a: Nat
2105  for b: Nat
2106  {Nat.mod(Nat.mul(a, b), a) == 0n : Nat}