law mul_dist_l

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

import Base

189law mul_dist_l:
190  for +k: Nat
191  for +a: Nat
192  for +b: Nat
193  {Nat.mul(k, Nat.add(a, b)) == Nat.add(Nat.mul(k, a), Nat.mul(k, b)) : Nat}