no goals
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
h : a ≠ c
⊢ ↑(lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c
field_simp [sub_ne_zero.2 h.symm, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c,
  lineMap_apply_module]