proposition: Lemma project_preserves_out : forall A B C A' B' C' P Q X Y, Out A B C -> ~Par A B X Y -> Proj A A' P Q X Y -> Proj B B' P Q X Y -> Proj C C' P Q X Y -> Out A' B' C'.
proof: Proof. intros. repeat split. intro. subst B'. unfold Out in H. spliter. unfold Proj in H1. unfold Proj in H2. spliter. induction H9; induction H13. assert(Par A A' B A'). apply (par_trans _ _ X Y); auto. apply par_symmetry. assumption. induction H14. apply H14. exists A'. split; Col. spliter. apply H0. apply par_symmetry. apply(par_col_par X Y A A' B). intro. subst B. tauto. apply par_symmetry. assumption. Col. subst A'. apply H0. apply par_left_comm. assumption. subst A'. contradiction. subst A'. contradiction. assert(HC:Col A B C). apply out_col in H. assumption. unfold Out in H. spliter. intro. subst C'. unfold Proj in H1 ,H3. spliter. induction H9; induction H13. assert(Par A A' C A'). apply (par_trans _ _ X Y). assumption. apply par_symmetry. assumption. induction H14. apply H14. exists A'. split; Col. spliter. apply H0. apply par_symmetry. apply (par_col_par X Y A A' B). intro. subst B. tauto. apply par_symmetry. assumption. ColR. subst A'. apply H0. apply par_symmetry. apply(par_col_par X Y A C B). intro. subst B. tauto. apply par_symmetry. apply par_left_comm. assumption. Col. subst A'. apply H0. apply par_symmetry. apply(par_col_par X Y A C B). intro. subst B. tauto. apply par_symmetry. assumption. Col. subst A'. contradiction. unfold Out in H. spliter. induction H5. left. apply (project_preserves_bet P Q X Y A B C A' B' C'); assumption. right. apply (project_preserves_bet P Q X Y A C B A' C' B'); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order