proposition: Lemma project_preserves_bet : forall A B X Y P Q R P' Q' R', Bet P Q R -> Proj P P' A B X Y -> Proj Q Q' A B X Y -> Proj R R' A B X Y -> Bet P' Q' R'.
proof: Proof. intros. assert(HH0:= H0). assert(HH1:=H1). assert(HH2:=H2). unfold Proj in HH0. unfold Proj in HH1. unfold Proj in HH2. spliter. clean_duplicated_hyps. assert(Col P' Q' R'). apply (col3 A B); Col. induction(eq_dec_points P Q). assert(P' = Q'). subst Q. eapply project_uniqueness. apply H0. assumption. subst Q'. Between. induction (eq_dec_points R Q). assert(R'=Q'). subst Q. eapply project_uniqueness. apply H2. assumption. subst Q'. Between. induction(eq_dec_points P' Q'). subst Q'. Between. induction(eq_dec_points R' Q'). subst Q'. Between. induction H17. apply par_distincts in H10. spliter. induction H12. apply par_distincts in H12. spliter. clear H20. assert(Par P P' Q Q'). eapply par_trans. apply H10. Par. assert(Par_strict Q Q' P P'). induction H20. apply par_strict_symmetry. assumption. spliter. assert(Q'=P'). apply (project_col_eq Q P Q' P' A B X Y); Col. subst Q'. tauto. assert(OS Q Q' P P'). eapply (par_strict_one_side). apply H21. Col. induction H7. assert(Par R R' Q Q'). eapply par_trans. apply H7. Par. assert(Par_strict Q Q' R R' ). induction H23. apply par_strict_symmetry. assumption. spliter. assert(Q'=R'). apply(project_col_eq Q R Q' R' A B X Y); Col. subst Q'. tauto. assert(OS Q Q' R R'). eapply (par_strict_one_side). apply H24. Col. assert(TS Q Q' P R). repeat split. auto. intro. apply H21. exists P. split; Col. intro. apply H24. exists R. split; Col. exists Q. split; Col. assert(TS Q Q' P' R'). eapply l9_8_2; [|apply H22]. apply l9_2. eapply l9_8_2. apply l9_2. apply H26. assumption. unfold TS in H27. spliter. ex_and H29 QQ. assert(QQ=Q'). assert(Col P' QQ R'). apply bet_col. assumption. eapply (l6_21 Q Q' P' R'); Col. intro. subst R'. apply between_equality in H30. subst QQ. contradiction. Between. subst QQ. assumption. subst R'. assert(TS Q Q' P' R). eapply l9_8_2; [|apply H22]. repeat split; Col. intro. assert(Q'=P'). apply project_col_eq with Q P A B X Y; Col. subst Q'. tauto. intro. assert(Q' = R). apply project_col_eq with Q R A B X Y; Col. subst Q'. tauto. exists Q. split; Col. unfold TS in H7. spliter. ex_and H24 QQ. assert(QQ=Q'). assert(Col P' QQ R). apply bet_col. assumption. eapply (l6_21 Q Q' P' R); Col. intro. subst R. apply between_equality in H25. subst QQ. contradiction. Between. subst QQ. assumption. subst Q'. induction H7. assert(HH:=parallel_existence X Y Q H14). ex_and HH Qx. ex_and H12 Qy. assert(Par Qx Qy P P'). eapply par_trans. apply par_symmetry. apply H19. Par. assert(Par_strict Qx Qy P P'). induction H21. assumption. spliter. assert(P' = Q). induction(eq_dec_points Qx Q). subst Qx. eapply(project_col_eq P Qy P' Q A B X Y); Col. apply par_col_project; auto. apply par_left_comm. Par. eapply(project_col_eq P Qx P' Q A B X Y); Col. apply par_col_project; auto. eapply (par_col_par_2 _ Qy); Col. Par. contradiction. assert(OS Qx Qy P P'). eapply (par_strict_one_side _ _ _ P'); Col. assert(Par Qx Qy R R'). eapply par_trans. apply par_symmetry. apply H19. Par. assert(Par_strict Qx Qy R R'). induction H24. assumption. spliter. assert(R' = Q). induction(eq_dec_points Qx Q). subst Qx. eapply(project_col_eq R Qy R' Q A B X Y); Col. apply par_col_project; auto. apply par_left_comm. Par. eapply(project_col_eq R Qx R' Q A B X Y); Col. apply par_col_project; auto. eapply (par_col_par_2 _ Qy); Col. Par. contradiction. assert(OS Qx Qy R R'). eapply (par_strict_one_side _ _ _ R'); Col. assert(TS Qx Qy P R). unfold TS. repeat split. auto. intro. apply H22. exists P. split; Col. intro. apply H25. exists R. split; Col. exists Q. split; Col. assert(TS Qx Qy P' R'). eapply l9_8_2; [|apply H23]. apply l9_2. eapply l9_8_2. eapply l9_2. apply H27. assumption. unfold TS in H28. spliter. ex_and H30 QQ. assert(QQ=Q). assert(Col P' QQ R'). apply bet_col. assumption. eapply (l6_21 Qx Qy P' R'); Col. intro. subst R'. apply between_equality in H31. subst QQ. contradiction. Between. subst QQ. assumption. subst R'. apply False_ind. assert(~ Col A B P). eapply project_not_col. apply H0. assumption. apply H7. assert(Col A Q R). ColR. assert(Col B Q R). ColR. apply bet_col in H. apply (col3 Q R); Col. subst P'. induction H12. induction H7. apply par_distincts in H10. apply par_distincts in H7. spliter. assert(Par Q Q' R R'). eapply par_trans. apply H10. Par. assert(Par_strict Q Q' R R'). induction H20. assumption. spliter. apply False_ind. apply H9. eapply (project_col_eq R Q _ _ A B X Y); Col. assert(OS Q Q' R R'). eapply (par_strict_one_side _ _ _ R'); Col. assert(TS Q Q' P R'). apply l9_2. eapply l9_8_2; [|apply H22]. repeat split; Col. intro. assert(Q'=R'). eapply (project_col_eq Q R _ _ A B X Y); Col. auto. intro. assert(Q' = P). eapply (project_col_eq Q P _ _ A B X Y); Col. auto. exists Q. split; Col. Between. unfold TS in H23. spliter. ex_and H25 QQ. assert(QQ=Q'). assert(Col P QQ R'). apply bet_col. assumption. eapply (l6_21 Q Q' P R'); Col. intro. subst P. apply between_equality in H26. subst QQ. contradiction. Between. subst QQ. assumption. subst R'. apply par_distincts in H10. spliter. assert(Q' = Q). eapply (l6_21 P R Q Q'); Col. assert_cols. intro. assert(~Col A B Q). eapply project_not_col. apply H1. auto. assert(Col A P R). ColR. assert(Col B P R). ColR. apply H19. eapply (col3 P R); Col. intro. subst R. apply between_identity in H. contradiction. subst Q'. assumption. subst Q'. induction H7. apply par_distincts in H7. spliter. assert(R = R'). eapply (l6_21 P Q R R'); Col. apply bet_col in H. Col. intro. assert(~Col A B R). eapply project_not_col. apply H2. auto. assert(Col A P Q). ColR. assert(Col B P Q). ColR. apply H18. eapply (col3 P Q); Col. contradiction. subst R'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors