law add_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:3974

import Base

3974# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
3975law add_mul_sym:
3976  for a: Nat
3977  for -b: Nat
3978  for c: Nat
3979  {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}