law mul_add_sym

bend-mathlib@0.8.1.0 · nat.bend:3984

import Base

3984# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
3985law mul_add_sym:
3986  for a: Nat
3987  for b: Nat
3988  for c: Nat
3989  {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}