proposition: Lemma l4_5 : forall A B C A' C', Bet A B C -> Cong A C A' C' -> exists B', Bet A' B' C' /\ Cong_3 A B C A' B' C'.
proof: Proof. intros. unfold Cong_3. assert (exists D', Bet C' A' D' /\ A' <> D') by (apply point_construction_different). ex_and H1 x'. prolong x' A' B' A B. prolong x' B' C'' B C. assert (Bet A' B' C'') by eBetween. assert (C'' = C'). eapply (construction_uniqueness x' A' ). auto. eBetween. apply (l2_11 A' B' C'' A B C);Between. eBetween. Cong. subst C''. exists B'. repeat split;Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch03_bet GeoCoq.Tarski_dev.Tactics.CongR