law esum_n

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1458

import Base

1458law esum_n:
1459  for +a: Nat
1460  for +h: Nat
1461  for +nn: Nat
1462  for +hle: {Nat.is_le(h, nn) == True{} : Bool}
1463  {Nat.add(Nat.add(a, h), Nat.sub(nn, h)) == Nat.add(a, nn) : Nat}