law add_mul

bend-mathlib@0.8.1.0 · nat.bend:288

import Base

288# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
289law add_mul:
290  for a: Nat
291  for -b: Nat
292  for c: Nat
293  {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}