proposition: Lemma bet_conga__bet : forall A B C A' B' C', Bet A B C -> CongA A B C A' B' C' -> Bet A' B' C'.
proof: Proof. intros. unfold CongA in H0. spliter. ex_and H4 A0. ex_and H5 C0. ex_and H4 A1. ex_and H5 C1. assert(Bet A0 B C0). apply outer_transitivity_between with C; auto. apply between_symmetry. apply outer_transitivity_between with A; Between. assert(Cong_3 A0 B C0 A1 B' C1). repeat split. apply cong_right_commutativity. eapply l2_11. apply between_symmetry. apply H4. apply H8. apply cong_left_commutativity. assumption. apply cong_symmetry. apply cong_right_commutativity. assumption. assumption. apply cong_right_commutativity. eapply l2_11. apply H6. apply between_symmetry. apply H10. apply cong_symmetry. apply cong_left_commutativity. assumption. apply cong_right_commutativity. assumption. assert(Bet A1 B' C1). eapply l4_6. apply H13. assumption. eapply between_inner_transitivity with C1; auto. eapply between_exchange3. apply between_symmetry. apply H8. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2