law mul_mod_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4435

import Base

4435# A multiple of b leaves no remainder modulo b: (a * b) % b = 0, reversed to rewrite toward the simple side.
4436law mul_mod_left_sym:
4437  for a: Nat
4438  for b: Nat
4439  {0n == Nat.mod(Nat.mul(a, b), b) : Nat}