digitslemmas2.lean

import data.nat.digits

lemma digits_eq_nil_iff_eq_zero (b n : ℕ) : digits b n = [] ↔ n = 0 :=
begin
  split,
  { intro h,
    have : of_digits b (digits b n) = of_digits b [], by rw h,
    convert this,
    rw of_digits_digits },
  { rintro rfl,
    simp }
end

lemma digits_ne_nil_iff_ne_zero (b n : ℕ) : digits b n ≠ [] ↔ n ≠ 0 := 
  ⟨λ h h', h $ (digits_eq_nil_iff_eq_zero _ _).mpr h', 
  λ h h', h $ (digits_eq_nil_iff_eq_zero _ _).mp h'⟩

@[simp] lemma of_digits_singleton {b n : ℕ} : of_digits b [n] = n := by simp [of_digits]

lemma pow_length_le_mul_of_digits {b : ℕ} {l : list ℕ} (hl : l ≠ []) (hl2 : l.last hl ≠ 0):
  (b + 2) ^ l.length ≤ (b + 2) * of_digits (b+2) l :=
begin
  rw [←list.init_append_last hl],
  simp only [list.length_append, list.length, zero_add, list.length_init, of_digits_append, list.length_init,
    of_digits_singleton, add_comm (l.length - 1), nat.pow_add, nat.pow_one],
  apply nat.mul_le_mul_left,
  refine le_trans _ (nat.le_add_left _ _),
  have : 1 ≤ l.last hl, { rwa [nat.succ_le_iff, nat.pos_iff_ne_zero] },
  convert nat.mul_le_mul_left _ this, rw [mul_one]
end

lemma last_digit_ne_zero (b m : ℕ) (hm : m ≠ 0) : 
  (digits b m).last ((digits_ne_nil_iff_ne_zero _ _).mpr hm) ≠ 0 :=
begin
  cases m,
  { contradiction },
  rcases b with _|_|b,
  { sorry },
  { sorry },
  { unfold digits, sorry }
end

lemma base_pow_length_digits_le' (b m : ℕ) (hm : m ≠ 0) : (b + 2) ^ ((digits (b + 2) m).length) ≤ (b + 2) * m :=
begin
  convert pow_length_le_mul_of_digits ((digits_ne_nil_iff_ne_zero _ _).mpr hm) (last_digit_ne_zero _ _ hm),
  rw of_digits_digits,
end