proposition: Lemma l9_4_2_aux : forall P Q A C R S U V, Le S C R A -> TS P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q -> Perp P Q C S -> Out R U A -> Out S V C -> TS P Q U V.
proof: Proof. intros. induction (eq_dec_points R S). subst S. assert (TT:= H0). unfold TS in H0. assert (~ Col A P Q). spliter. assumption. spliter. clear H0. assert (P <> Q). intro. subst Q. Col. ex_and H9 T. induction (eq_dec_points R T). subst T. clear H9 H3. apply (out_out_two_sides P Q A C U V R); auto using l6_6, bet_col with col. assert (Perp R T A R) by (eapply perp_col2 with P Q;Col). apply perp_perp_in in H12. apply perp_in_comm in H12. eapply perp_in_per in H12. assert (Perp R T C R) by (eapply perp_col2 with P Q;Col). apply perp_perp_in in H13. apply perp_in_comm in H13. eapply perp_in_per in H13. assert (R = T). apply (l8_6 C R T A). apply l8_2;auto. apply l8_2;auto. Between. subst. intuition. assert(P <> Q). apply perp_distinct in H4. spliter. assumption. assert (TS R S A C). eapply (col_preserves_two_sides P Q). apply H7. apply col_permutation_1. assumption. apply col_permutation_1. assumption. assumption. eapply (col_preserves_two_sides R S). assumption. eapply col_permutation_1. eapply col_transitivity_1. apply H8. apply col_permutation_1. assumption. apply col_permutation_1. assumption. apply col_permutation_1. eapply (col_transitivity_1 _ P). auto. apply col_permutation_3. assumption. apply col_permutation_3. assumption. assert (Perp R S A R). eapply perp_col2. apply H2. assumption. apply col_permutation_1. assumption. apply col_permutation_1. assumption. assert (Perp R S C S). eapply perp_col2. apply H4. assumption. apply col_permutation_1. assumption. apply col_permutation_1. assumption. assert (HH9:=H9). unfold TS in HH9. assert (~ Col A R S). spliter. assumption. spliter. ex_and H15 T. unfold Le in H. ex_and H C'. assert (exists M, Midpoint M S R /\ Midpoint M C C'). eapply (l8_24 S R C A C' T). apply perp_sym. apply perp_left_comm. assumption. apply perp_sym. apply perp_left_comm. assumption. apply col_permutation_3. assumption. apply between_symmetry. assumption. assumption. assumption. ex_and H18 M. double U M U'. assert (R <> U). intro. subst U. unfold Out in H5. spliter. absurde. assert (TS R S U U'). eapply mid_two_sides. apply l7_2. apply H18. intro. apply H13. eapply col_permutation_2. eapply col_transitivity_1. apply H21. apply col_permutation_5. assumption. induction H5. spliter. induction H24. unfold Col. left. assumption. unfold Col. right; left. apply between_symmetry. assumption. assumption. apply l9_2. eapply l9_3. apply l9_2. apply H22. unfold Col. right; right. apply midpoint_bet. apply H18. apply l7_2. assumption. apply col_trivial_3. assert (forall X Y, Midpoint M X Y -> (Out R X A <-> Out S C Y)). eapply l9_4_1. apply H9. apply col_trivial_1. assumption. apply col_trivial_3. assumption. apply l7_2. assumption. assert (Out R U A <-> Out S C U'). eapply H23. assumption. destruct H24. eapply l6_7. apply l6_6. apply H24. assumption. apply l6_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar