digits'.lean

import data.nat.digits

lemma nat.div_lt_of_le : ∀ {n m k : ℕ} (h0 : n > 0) (h1 : m > 1) (hkn : k ≤ n), k / m < n
| 0     m k h0 h1 hkn := absurd h0 dec_trivial
| 1     m 0 h0 h1 hkn := by rwa nat.zero_div
| 1     m 1 h0 h1 hkn :=
  have ¬ (0 < m ∧ m ≤ 1), from λ h, absurd (@lt_of_lt_of_le ℕ 
    (show preorder ℕ, from @partial_order.to_preorder ℕ (@linear_order.to_partial_order ℕ nat.linear_order))
     _ _ _ h1 h.2) dec_trivial,
  by rw [nat.div_def_aux, dif_neg this]; exact dec_trivial
| 1     m (k+2) h0 h1 hkn := absurd hkn dec_trivial
| (n+2) m k h0 h1 hkn := begin
  rw [nat.div_def_aux],
  cases decidable.em (0 < m ∧ m ≤ k) with h h,
  { rw [dif_pos h],
    refine nat.succ_lt_succ _,
    refine nat.div_lt_of_le (nat.succ_pos _) h1 _,
    cases m with m,
    { exact absurd h.1 dec_trivial },
    { cases m with m,
      { exact absurd h1 dec_trivial },
      { clear h1 h,
        induction m with m ih,
        { cases k with k,
          { exact nat.zero_le _ },
          { cases k with k,
            { exact nat.zero_le _ },
            { rw [nat.sub_succ, nat.sub_succ, nat.sub_zero, nat.pred_succ,
                nat.pred_succ],
              exact @linear_order.le_trans ℕ nat.linear_order _ _ _ 
                (nat.le_succ k) (nat.le_of_succ_le_succ hkn) } } },
        { cases k with k,
          { rw [nat.zero_sub], exact nat.zero_le _ },
          { rw [nat.succ_sub_succ],
            refine @linear_order.le_trans ℕ nat.linear_order _ _ _ _ ih,
            refine nat.sub_le_sub_right _ _,
            exact nat.le_succ _ } } } } },
  { rw dif_neg h,
    exact nat.succ_pos _ }
end

lemma nat.div_lt_self'' {n m : ℕ} (h0 : n > 0)  (hm : m > 1) : n / m < n :=
nat.div_lt_of_le h0 hm (le_refl _)

def f : ℕ → ℕ
| n :=
  if h : 0 < n
  then have n - 1 < n, from nat.sub_lt h zero_lt_one,
    f (n - 1)
  else 0

def digits_aux' (b : ℕ) (h : 2 ≤ b) : ℕ → list ℕ
| 0 := []
| (n+1) :=
  have (n+1)/b < n+1 := nat.div_lt_self'' (nat.succ_pos _) h,
  (n+1) % b :: digits_aux' ((n+1)/b)

def digits' : ℕ → ℕ → list ℕ
| 0 := digits_aux_0
| 1 := digits_aux_1
| (b+2) := digits_aux' (b+2) dec_trivial

theorem test (b n : ℕ) : digits' (b+2) (n+1) = (n+1)%(b+2) :: digits' (b+2) ((n+1)/(b+2)) := rfl -- works
theorem test' : digits' (0+2) (1+1) = (1+1)%(0+2) :: digits' (0+2) ((1+1)/(0+2)) := rfl