law mul_dist

bend-ml-nat-lemmas@0.1.2.0 · main.bend:140

import Base

140law mul_dist:
141  for  a: Nat
142  for -b: Nat
143  for +c: Nat
144  {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}