law pow_add

lawful-words@0.1.0.0 · proof_nat.bend:1375

import Base

1375law pow_add:
1376  for +b: Nat
1377  for +j: Nat
1378  for +k: Nat
1379  {Nat.pow(b, Nat.add(j, k)) == Nat.mul(Nat.pow(b, j), Nat.pow(b, k)) : Nat}