def pk.le_sub

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

import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOF

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

67# q - r <= q
68def pk.le_sub(+q: Nat, +r: Nat) -> {Nat.is_le(Nat.sub(q, r), q) == True{} : Bool}:
69  match q r:
70    case 0n _:
71      {==}
72    case 1n+qp 0n:
73      UL.nat_le_refl(qp)
74    case 1n+qp 1n+rp:
75      pk.le_step(Nat.sub(qp, rp), qp)(pk.le_sub(qp, rp))

Uses (6)

Used by (1)

bend-osdev-pkcs7@0.1.0.0/PROOF:pk.main