def pk.sub_add_r

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:138

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

138# (1 + m + r) - r = 1 + m
139def pk.sub_add_r(+m: Nat, +r: Nat) -> {Nat.sub(1n+Nat.add(m, r), r) == 1n+m : Nat}:
140  match r:
141    case 0n:
142      %UL.nat_add_zero(m) : {Nat.sub(1n+Nat.add(m, 0n), 0n) == 1n+_ : Nat}
143      {==}
144    case 1n+rp:
145      %Equal.sym(Nat, Nat.add(m, 1n+rp), 1n+Nat.add(m, rp), UL.nat_add_succ(m, rp)) : {Nat.sub(1n+_, 1n+rp) == 1n+m : Nat}
146      pk.sub_add_r(m, rp)