law cmp_dbl

lawful-words@0.1.0.0 · proof_word.bend:164

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

164law cmp_dbl:
165  for +x: Nat
166  for +y: Nat
167  for +a: Bool
168  for +b: Bool
169  {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(Nat.add(N.bn(a), Nat.double(x)), Nat.add(N.bn(b), Nat.double(y))) : Cmp}