def pk.mod_le

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

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

148# the remainder is at most q
149def pk.mod_le(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Nat.is_le(Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)), q) == True{} : Bool}:
150  match a:
151    case 0n:
152      inv => %inv : {Nat.is_le(r, _) == True{} : Bool}
153        UL.nat_le_add(r, m)
154    case 1n+ap:
155      match m:
156        case 0n:
157          inv => pk.mod_le(ap, r, 1n+d, 0n, q)(Equal.trans(Nat, Nat.add(r, 0n), r, q, UL.nat_add_zero(r), inv))
158        case 1n+mp:
159          inv => pk.mod_le(ap, mp, d, 1n+r, q)(Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), q, UL.nat_add_succ(mp, r), inv))