English
powHalf(n+1) + powHalf(n+1) is equivalent to powHalf(n).
Русский
powHalf(n+1) + powHalf(n+1) эквивалентно powHalf(n).
LaTeX
$$$\text{powHalf}(n+1) + \text{powHalf}(n+1) \approx \text{powHalf}(n)$$$
Lean4
theorem add_powHalf_succ_self_eq_powHalf (n) : powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n :=
by
induction n using Nat.strong_induction_on with
| _ n hn
constructor <;> rw [le_iff_forall_lf] <;> constructor
· rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt
·
calc
0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _
_ < powHalf n := powHalf_succ_lt_powHalf n
·
calc
powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _
_ < powHalf n := powHalf_succ_lt_powHalf n
· rcases n with - | n
· rintro ⟨⟩
rintro ⟨⟩
apply lf_of_moveRight_le
swap
· exact Sum.inl default
calc
powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ :=
add_le_add_left (powHalf_succ_le_powHalf _) _
_ ≈ powHalf n := hn _ (Nat.lt_succ_self n)
· simp only [powHalf_moveLeft, forall_const]
apply lf_of_lt
calc
0 ≈ 0 + 0 := Equiv.symm (add_zero_equiv 0)
_ ≤ powHalf n.succ + 0 := (add_le_add_right (zero_le_powHalf _) _)
_ < powHalf n.succ + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
· rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt
·
calc
powHalf n ≈ powHalf n + 0 := Equiv.symm (add_zero_equiv _)
_ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
·
calc
powHalf n ≈ 0 + powHalf n := Equiv.symm (zero_add_equiv _)
_ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _
