Theorem: UInt.toNat_lt (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a < 2 ^ length α
Tactic:
rw [←ofNat_toNat a, toNat_ofNat]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α < 2 ^ length α

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α < 2 ^ length α
Tactic:
exact Nat.mod_lt (toNat a) (y:=2^(length α)) (Nat.pos_pow_of_pos _ (Nat.zero_lt_succ 1))
State after:
no goals