law mul_add_r

lawful-words@0.1.0.0 · proof_nat.bend:453

import Base

453law mul_add_r:
454  for +a: Nat
455  for +b: Nat
456  for +c: Nat
457  {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}