law mul_sub

bend-mathlib@0.8.1.0 · nat.bend:2354

import Base

2354# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k.
2355law mul_sub:
2356  for n: Nat
2357  for m: Nat
2358  for k: Nat
2359  {Nat.mul(n, Nat.sub(m, k)) == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}