theorem Nat.power_of_two_go_eq_eq (n : Nat) (p : n >0) : Nat.nextPowerOfTwo.go n n p = n := by
  unfold Nat.nextPowerOfTwo.go
  simp_arith

theorem Nat.smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < m :=
  if h₁ : m ≤ n  then
    by have h₂ := Nat.pow_le_pow_of_le_right (q) h₁
       have h₃ := Nat.lt_of_le_of_lt h₂ p
       simp_arith at h₃
  else
    by rewrite[Nat.not_ge_eq] at h₁
       trivial

private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power < n) : power * 2 ≤ n := by
  unfold Nat.isPowerOfTwo at h₁ h₂
  have ⟨k, h₄⟩ := h₁
  have ⟨l, h₅⟩ := h₂
  rewrite [h₅]
  rewrite[←Nat.pow_succ 2 l]
  rewrite[h₄]
  have h₆ : 2 > 0 := by decide
  apply (Nat.pow_le_pow_of_le_right h₆)
  rewrite [h₅] at h₃
  rewrite [h₄] at h₃
  have h₃ := Nat.smaller_smaller_exp h₃
  simp_arith at h₃
  assumption

private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by
  unfold Nat.nextPowerOfTwo.go
  split
  case inl h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄)
  case inr h₄ => rewrite[Nat.not_lt_eq power n] at h₄
                 exact Nat.le_antisymm h₃ h₄
termination_by power_of_two_go_one_eq _ p _ _ _ => n - p
decreasing_by
  simp_wf
  have := Nat.pos_of_isPowerOfTwo h₂
  apply Nat.nextPowerOfTwo_dec <;> assumption

private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.nextPowerOfTwo = n) := by
  intro h₁
  unfold Nat.nextPowerOfTwo
  apply power_of_two_go_one_eq
  case h₁ => assumption
  case h₂ => exact Nat.one_isPowerOfTwo
  case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁)

private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by
  have h₂ := Nat.isPowerOfTwo_nextPowerOfTwo n
  intro h₁
  revert h₂
  rewrite[h₁]
  intro
  assumption

theorem Nat.power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPowerOfTwo = n) :=
  Iff.intro (power_of_two_eq_power_of_two n) (eq_power_of_two_power_of_two n)

theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).isPowerOfTwo :=
  have h₁ : n.isPowerOfTwo → (2*n).isPowerOfTwo := by
    simp[Nat.mul_comm]
    apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo
  have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo :=
    if h₂ : n.nextPowerOfTwo = n then by
      simp[power_of_two_iff_next_power_eq,h₂]
    else by
      intro h₃
      simp[←power_of_two_iff_next_power_eq] at h₂
      have h₅ := h₃
      unfold Nat.isPowerOfTwo at h₃
      let ⟨k,h₄⟩ := h₃
      cases n with
      | zero => contradiction
      | succ m => cases k with
        | zero => simp_arith at h₄
                  have h₆ (m : Nat) : 2*m+2 > 2^0 := by
                    induction m with
                    | zero => decide
                    | succ o o_ih => simp_arith at *
                                     have h₆ := Nat.le_step $ Nat.le_step o_ih
                                     simp_arith at h₆
                                     assumption
                  have h₆ := Nat.ne_of_lt (h₆ m)
                  simp_arith at h₆
                  rewrite[h₄] at h₆ --why is this needed?!?
                  contradiction
        | succ l => rewrite[Nat.pow_succ 2 l] at h₄
                    rewrite[Nat.mul_comm (2^l) 2] at h₄
                    have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄
                    exists l
  Iff.intro h₁ h₂