lemmas for Nat.digits

Stream: general

[Frederick Pu]

do the following lemmas exist for Nat.digits?

example (x b : ℕ) (hb : b > 1) (hx : (Nat.digits b x).length = 1) : Nat.digits b x = [x] := by sorry
example (x b : ℕ) (hb : b > 1) (hx : x > 0) : (Nat.digits b x).length > 0 := by sorry

[Matt Diamond]

docs#Nat.digits_len gets you most of the way toward proving the 2nd one:

example (x b : ℕ) (hb : b > 1) (hx : x > 0) : (Nat.digits b x).length > 0 := by
  rw [Nat.digits_len _ _ hb hx.ne']
  exact Nat.zero_lt_succ _

[Daniel Weber]

Could you do the first with docs#Nat.digits_of_lt ?

[Frederick Pu]

but we also need to prove that if (Nat.digits b x).length = 1 then x < b

[Kevin Buzzard]

Looks like digits_len reduces this to docs#Nat.log_eq_zero_iff

[Kevin Buzzard]

Probably one should prove x < b^length if that's not already there

[Frederick Pu]

doesn't Nat.digits_len basically do that?