law sub_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:4541

import Base

4541# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k, reversed to rewrite toward the simple side.
4542law sub_mul_sym:
4543  for n: Nat
4544  for m: Nat
4545  for k: Nat
4546  {Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) == Nat.mul(Nat.sub(n, m), k) : Nat}