Clean up proof of lsb stuff

Changes

1 changed files (+4/-7)

• Main.lean
  • @@ -36,20 +36,17 @@ def merge [Ord α] (xs : List α) (ys : List α) : List α :=
    | .gt => y' :: merge (x'::xs') ys' - theorem blah (i : ℕ) : i ≠ 0 → i / 2 < i := by - exact fun a => Nat.bitwise_rec_lemma a + def lsb (i : Nat) : Nat := if i = 0 then 0 else if i % 2 == 1 then 1 else 2 * lsb (i / 2) termination_by i decreasing_by - cases i - case zero => + if h : i = 0 then simp contradiction - case succ => - apply blah - simp + else + exact Nat.bitwise_rec_lemma h theorem lsb_le_i (i : Nat) : lsb i ≤ i := by if h₁ : i = 0 then