law sub_mul

bend-mathlib@0.8.1.0 · nat.bend:2335

import Base

2335# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k.
2336law sub_mul:
2337  for n: Nat
2338  for m: Nat
2339  for k: Nat
2340  {Nat.mul(Nat.sub(n, m), k) == Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) : Nat}