def div10_lt

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

1271# n / 10 < n for n >= 1.
1272def div10_lt(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(n, 10n), n) == True{} : Bool}:
1273  match n:
1274    case 0n:
1275      Empty.absurd({Nat.is_lt(Nat.div(0n, 10n), 0n) == True{} : Bool}, L.false_true(h))
1276    case 1n+ +m:
1277      +e = NR.le_div(9n, 1n+m, 1n+m)
1278      +f = N.lt_not_le(m, Nat.add(9n, Nat.mul(m, 10n)), lt9(m))
1279      N.not_le_lt(1n+m, Nat.div(1n+m, 10n), Equal.trans(Bool, Nat.is_le(1n+m, Nat.div(1n+m, 10n)), Nat.is_le(Nat.mul(1n+m, 10n), 1n+m), False{}, e, f))