def dd_n

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:1205

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

1205def dd_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)) == n : Nat}:
1206  match n:
1207    case 0n:
1208      {==}
1209    case 1n:
1210      {==}
1211    case 2n:
1212      {==}
1213    case 3n:
1214      {==}
1215    case 4n:
1216      {==}
1217    case 5n:
1218      {==}
1219    case 6n:
1220      {==}
1221    case 7n:
1222      {==}
1223    case 8n:
1224      {==}
1225    case 9n:
1226      {==}
1227    case 10n+r:
1228      Empty.absurd({U32.to_nat(U32.sub(U32.add(48, U32.from_nat(10n+r)), 48)) == 10n+r : Nat}, N.lt_zero_absurd(r, h))