proposition: Lemma bet3_cong3_bet : forall A B C D D', A <> B -> A <> C -> A <> D -> Bet D A C -> Bet A C B -> Bet D C D' -> Cong A B C D -> Cong A D B C -> Cong D C C D' -> Bet C B D'.
proof: Proof. intros. assert(Bet D C B). eBetween. assert(B <> C). intro. subst C. apply cong_identity in H6. contradiction. assert(D' <> C). intro. subst D'. apply cong_identity in H7. subst D. apply cong_identity in H5. contradiction. assert(D <> C). intro. subst D. apply cong_identity in H5. contradiction. assert (Out C B D'). repeat split; auto. eapply (l5_2 D); auto. assert(Out D B D'). repeat split; auto. intro. subst D. apply between_identity in H8. contradiction. intro. subst D'. apply between_identity in H4. contradiction. eapply (l5_1 _ C); auto. assert(Le D A D C). unfold Le. exists A. split; Cong. assert(Le D B D D'). eapply (bet2_le2__le1346 _ A _ _ C). eBetween. assumption. assumption. apply cong__le; CongR. apply (between_exchange3 D); auto. apply l6_13_1; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel