def internal_u32_inc_exact

bend-mathlib@0.8.1.0 · u32.bend:663

import bend-mathlib@0.8.1.0/u32.bend as U32

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

663def internal_u32_inc_exact(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(1n+U32.to_nat(a), m)) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
664  match a:
665    case U32{+w}:
666      word_inc_exact(32n, w, internal_bound(1n+Word.to_nat(32n, w), m, e, h))

Uses (9)

Used by (2)