def pk.sub_succ

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

import Base

77# r <= q gives (1 + q) - r = 1 + (q - r)
78def pk.sub_succ(+r: Nat, +q: Nat) -> {Nat.is_le(r, q) == True{} : Bool} -> {Nat.sub(1n+q, r) == 1n+Nat.sub(q, r) : Nat}:
79  match r q:
80    case 0n _:
81      h => %Equal.sym(Nat, Nat.sub(q, 0n), q, pk.sub_zero(q)) : {1n+q == 1n+_ : Nat}
82        {==}
83    case 1n+rp 0n:
84      h => pk.absurd({Nat.sub(1n, 1n+rp) == 1n+Nat.sub(0n, 1n+rp) : Nat}, h)
85    case 1n+rp 1n+qp:
86      h => pk.sub_succ(rp, qp)(h)