proposition: Lemma l4_6 : forall A B C A' B' C', Bet A B C -> Cong_3 A B C A' B' C' -> Bet A' B' C'.
proof: Proof. unfold Cong_3. intros. assert (exists B'', Bet A' B'' C' /\ Cong_3 A B C A' B'' C') by (eapply l4_5;intuition). ex_and H1 x. unfold Cong_3 in *;spliter. assert (Cong_3 A' x C' A' B' C'). unfold Cong_3;repeat split; Cong. apply cong_transitivity with A B; Cong. apply cong_transitivity with B C; Cong. unfold Cong_3 in H7;spliter. assert (IFSC A' x C' x A' x C' B') by (unfold IFSC;repeat split;Cong). assert (Cong x x x B') by (eapply l4_2;apply H10). treat_equalities. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch03_bet GeoCoq.Tarski_dev.Tactics.CongR