law mul_add

lawful-words@0.1.0.0 · proof_nat.bend:439

import Base

439law mul_add:
440  for +a: Nat
441  for +b: Nat
442  for +c: Nat
443  {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}