def na.sub_add

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1684

import Base

1684# (a + b) - b == a
1685def na.sub_add(+a: Nat, +b: Nat) -> {Nat.sub(Nat.add(a, b), b) == a : Nat}:
1686  match b:
1687    case 0n:
1688      %Equal.sym(Nat, Nat.add(a, 0n), a, na.add_zero(a)) : {Nat.sub(_, 0n) == a : Nat}
1689      na.sub_zero(a)
1690    case 1n+p:
1691      %Equal.sym(Nat, Nat.add(a, 1n+p), 1n+Nat.add(a, p), na.add_succ(a, p)) : {Nat.sub(_, 1n+p) == a : Nat}
1692      na.sub_add(a, p)