proposition: Lemma ex_point_lg_bet : forall l A M, Q_Cong l -> exists B : Tpoint, l M B /\ Bet A M B.
proof: Proof. intros. assert(HH:= H). unfold Q_Cong in HH. ex_and HH X. ex_and H0 Y. assert(HP:= H1 X Y). destruct HP. assert(l X Y). apply H0. apply cong_reflexivity. prolong A M B X Y. exists B. split; auto. eapply (lg_cong_lg l X Y); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1