law mul_succ

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

import Base

109law mul_succ:
110  for +a: Nat
111  for +b: Nat
112  {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}