IMO 2014 P4 - Proving Line Intersection with Strict Betweenn

Stream: Is there code for X?

[Li Jiale]

Problem Statement (IMO 2014 P4)

In acute triangle ABC, points P and Q lie on BC such that ∠PAB = ∠BCA and ∠CAQ = ∠ABC. Let M and N be points such that P is the midpoint of AM and Q is the midpoint of AN.

Lean goal (no betweenness, just lines):

theorem BM_CN_intersect : ∃ X : Pt, X ∈ line[ℝ, cfg.B, cfg.M] ∧ X ∈ line[ℝ, cfg.C, cfg.N]

What’s the recommended approach/lemmas in mathlib?

Is there a standard “two non-parallel lines intersect” lemma for AffineSubspace lines, e.g.

lemma lines_intersect_of_not_parallel {A B C D : Pt}
    (h : ¬(line[ℝ, A, B] ∥ line[ℝ, C, D])) :
    ∃ X : Pt, X ∈ line[ℝ, A, B] ∧ X ∈ line[ℝ, C, D] := by
  sorry

and if so, what’s its name / minimal hypotheses?

If the “non-parallel ⇒ intersection” route is the right one, what’s the cleanest way in mathlib to turn these angle facts (or a simpler consequence of them) into ¬ (line[ℝ, B, M]).Parallel (line[ℝ, C, N]) ？

Any small pattern/lemma name pointers would be super helpful (either a ready lemma for lines, or a canonical way to show not_parallel in this setting). Thanks!