proposition: Lemma segment_construction_2 : forall A Q B C, A <> Q -> exists X, (Bet Q A X \/ Bet Q X A) /\ Cong Q X B C.
proof: Proof. intros. prolong A Q A' A Q. prolong A' Q X B C. exists X. show_distinct A' Q. solve [intuition]. split; try assumption. eapply (l5_2 A' Q); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col