law mul_sub_sym

bend-mathlib@0.8.1.0 · nat.bend:4551

import Base

4551# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k, reversed to rewrite toward the simple side.
4552law mul_sub_sym:
4553  for n: Nat
4554  for m: Nat
4555  for k: Nat
4556  {Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) == Nat.mul(n, Nat.sub(m, k)) : Nat}