law al_k

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1050

import Base

1050# x = 4a + k with k + h = 4 gives x + h = 4(a + 1).
1051law al_k:
1052  for +x: Nat
1053  for +a: Nat
1054  for +k: Nat
1055  for +h: Nat
1056  for +ex: {x == Nat.add(Nat.mul(a, 4n), k) : Nat}
1057  for +ek: {Nat.add(k, h) == 4n : Nat}
1058  {Nat.add(x, h) == Nat.mul(1n+a, 4n) : Nat}