law mul_add

bend-mathlib@0.8.1.0 · nat.bend:305

import Base

305# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
306law mul_add:
307  for a: Nat
308  for b: Nat
309  for c: Nat
310  {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}