proposition: Lemma l5_1 : forall A B C D, A <> B -> Bet A B C -> Bet A B D -> Bet A C D \/ Bet A D C.
proof: Proof. intros. prolong A D C' C D. prolong A C D' C D. prolong A C' B' C B. prolong A D' B'' D B. assert (Cong B C' B'' C). apply (l2_11 B D C' B'' D' C). apply between_exchange3 with A; Between. apply between_inner_transitivity with A; Between. Cong. apply cong_transitivity with C D; Cong. assert (Cong B B' B'' B). { apply (l2_11 B C' B' B'' C B); Cong. { assert (Bet A B C'); [|eBetween]. induction (eq_dec_points B D); [treat_equalities; auto|]. apply between_symmetry. apply outer_transitivity_between2 with D; eBetween. } { induction (eq_dec_points C D'); [treat_equalities; eBetween|]. apply outer_transitivity_between2 with D'; eBetween. } } assert(B'' = B'). apply (construction_uniqueness A B B B''); Cong. apply between_exchange4 with D'; Between; apply between_exchange4 with C; Between. apply between_exchange4 with C'; Between; apply between_exchange4 with D; Between. subst B''. assert (Bet B C D') by (apply between_exchange3 with A; assumption). assert (FSC B C D' C' B' C' D C). repeat split; Cong. left; apply between_exchange3 with A; Between. apply (l2_11 B C D' B' C' D); Cong. apply between_symmetry. apply between_exchange3 with A; assumption. apply cong_transitivity with C D; Cong. apply cong_transitivity with C D; Cong. induction (eq_dec_points B C). subst C; auto. assert (Cong D' C' D C) by (eapply l4_16; try apply H13; assumption). assert (exists E, Bet C E C' /\ Bet D E D') by (apply inner_pasch with A; Between). ex_and H16 E. assert (IFSC D E D' C D E D' C') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong). assert (IFSC C E C' D C E C' D') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong). assert (Cong E C E C') by (eapply l4_2; try apply H18; auto). assert (Cong E D E D') by (eapply l4_2; try apply H19; auto). induction (eq_dec_points C C'). subst C'; right; assumption. show_distinct C D'. auto. prolong C' C P C D'. prolong D' C R C E. prolong P R Q R P. assert (FSC D' C R P P C E D'). repeat split; Col; Cong. apply l2_11 with C C; Cong. apply between_inner_transitivity with C'; Between. assert (Cong R P E D') by (eauto using l4_16). assert (Cong R Q E D). eapply cong_transitivity. apply cong_transitivity with R P; Cong. apply cong_transitivity with E D'; Cong. assert (FSC D' E D C P R Q C). repeat split; Col; Cong. eapply (l2_11 D' E D P R Q); Between; Cong. assert (Cong D C Q C). induction (eq_dec_points D' E). unfold IFSC, Cong_3 in *; spliter; treat_equalities; Cong. apply l4_16 with D' E P R; assumption. assert (Cong C P C Q). unfold FSC, Cong_3 in *; spliter. apply cong_transitivity with C D; Cong. apply cong_transitivity with C D'; Cong. show_distinct R C. auto. assert (Cong D' P D' Q) by (apply (l4_17 R C); unfold Col; Between; Cong). assert (Cong B P B Q). apply l4_17 with C D'; Col. assert (Cong B' P B' Q). apply (l4_17 C D'); Cong. left. apply between_exchange3 with A; assumption. assert (Cong C' P C' Q). assert (Bet B C' B'). apply between_exchange3 with A; try assumption. apply between_exchange4 with D; try assumption. eapply l4_17 with B B'; Cong; Col. intro; treat_equalities; auto. assert (Cong P P P Q). apply l4_17 with C C'; Col. treat_equalities. left; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col