law mul_mod_left

bend-mathlib@0.8.1.0 · nat.bend:2087

import Base

2087# A multiple of b leaves no remainder modulo b: (a * b) % b = 0.
2088law mul_mod_left:
2089  for a: Nat
2090  for b: Nat
2091  {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}