Theorem: sub_half_of_even (Fl/Lemmas.lean)

State before:
x : ℕ
d : 2 ∣ x
⊢ x - x / 2 = x / 2
Tactic:
have h₀ : 2 - 1 = 1 := by rw [← one_add_one_eq_two, add_tsub_cancel_right]
State after:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
⊢ x - x / 2 = x / 2

State before:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
⊢ x - x / 2 = x / 2
Tactic:
have h₁ := sub_div_of_pos_of_dvd two_pos d
State after:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = (2 - 1) * x / 2
⊢ x - x / 2 = x / 2

State before:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = (2 - 1) * x / 2
⊢ x - x / 2 = x / 2
Tactic:
rewrite [h₀, one_mul] at h₁
State after:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = x / 2
⊢ x - x / 2 = x / 2

State before:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = x / 2
⊢ x - x / 2 = x / 2
Tactic:
exact h₁
State after:
no goals

State before:
x : ℕ
d : 2 ∣ x
⊢ 2 - 1 = 1
Tactic:
rw [← one_add_one_eq_two, add_tsub_cancel_right]
State after:
no goals