Theorem: sub_div_of_pos_of_dvd (Fl/Lemmas.lean)

State before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
⊢ x - x / d = (d - 1) * x / d
Tactic:
have hdvd' : d ∣ (d - 1) * x := Nat.dvd_trans hdvd (Nat.dvd_mul_left _ _)
State after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x - x / d = (d - 1) * x / d

State before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x - x / d = (d - 1) * x / d
Tactic:
apply Nat.eq_of_mul_eq_mul_right hpos
State after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ (x - x / d) * d = (d - 1) * x / d * d

State before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ (x - x / d) * d = (d - 1) * x / d * d
Tactic:
rewrite [Nat.mul_sub_right_distrib]
State after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x / d * d = (d - 1) * x / d * d

State before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x / d * d = (d - 1) * x / d * d
Tactic:
rewrite [Nat.div_mul_cancel hdvd, Nat.div_mul_cancel hdvd']
State after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = (d - 1) * x

State before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = (d - 1) * x
Tactic:
rewrite [Nat.sub_one, Nat.mul_pred_left]
State after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = d * x - x

State before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = d * x - x
Tactic:
rw [Nat.mul_comm]
State after:
no goals