Is there a better way of writing complex geometric theorem statements?

[jjdishere]

We encountered the following dilemma:

Short proofs need to be inserted in the statement of a theorem.
such as LIN A B (ne_of_colinear h).1

Is there a form of stating theorems such that:

1. there is a context (just as when we are writing proofs), we can freely add variables by have or let, easy to use them
2. the new variable created by let can be further used in the proof

There are several solutions:

1. The current solution is

variable {A B C D : P} {habc : \not colinear A B C}
lemma A_ne_B : A \ne B := (ne_of_colinear habc).2.2

theorem ... :  ... LIN B A (A_ne_B (habc := habc)) ...

Bad:
since each lemma is a independent environment, we must provide habc in A_ne_B (habc := habc).
Good:
we can use A_ne_B (habc := habc) in the proof.

2. Another possible solution is

theorem {A B C D : P}  {habc : \not colinear A B C} : let A_ne_B := (ne_of_colinear habc).2.2; ... LIN B A (A_ne_B) ... := 

Bad: A_ne_B cannot be used in theorem, a simp will eliminate all let in the goal and make the goal unreadable.
and one cannot use those let in the proof
Good : There is a context, no need to write A_ne_B (habc := habc)

3. Another possible solution is
   Based on 2, one can just copy those let in the statement into proof.

4. A totally different solution is
   Use Option. LIN A B only defines an Option (Line P), Line.inx defines an element in Option P, everything has an option version colinear A B C is Option Prop, if B is .none, then colinear A B C is .none

Then the conditions of an exercise should be enough to show all of the following constructions are not .none.

Is there a better solution?