law nk

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:169

import Base

169law nk:
170  for +x: Nat
171  for +A: Nat
172  for +B: Nat
173  for +E: Nat
174  {Nat.mul(x, Nat.add(1n, Nat.add(Nat.mul(1n, A), Nat.add(Nat.mul(1n, B), Nat.mul(1n, E))))) == Nat.add(x, Nat.add(Nat.mul(x, A), Nat.add(Nat.mul(x, B), Nat.mul(x, E)))) : Nat}