Theorem: Nat.digit_lt_base (One.lean)

State before:
base n index : ℕ
P : base > 0
⊢ digit base n index < base
Tactic:
unfold Nat.digit
State after:
base n index : ℕ
P : base > 0
⊢ n / base ^ index % base < base

State before:
base n index : ℕ
P : base > 0
⊢ n / base ^ index % base < base
Tactic:
apply Nat.mod_lt _ P
State after:
no goals