proposition: Lemma l9_4_1_aux : forall P Q A C R S M, 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 -> Midpoint M R S -> (forall U C',Midpoint M U C' -> (Out R U A <-> Out S C C')).
proof: Proof. intros. induction (eq_dec_points R S). subst S. apply l7_3 in H5. subst R. unfold TS in H0. assert (~ Col A P Q). spliter. assumption. spliter. clear H0. assert (P <> Q). intro. subst Q. Col. ex_and H8 T. induction (eq_dec_points M T). subst T. split. intro. unfold Out in *. spliter. repeat split. intro. subst C. apply perp_distinct in H4. spliter. absurde. intro. subst C'. apply l7_2 in H6. eapply (symmetric_point_uniqueness _ _ M) in H6. apply H10. apply sym_equal. apply H6. apply l7_3_2. induction H12. assert (Bet U M C). eapply between_exchange3. apply between_symmetry. apply H12. assumption. unfold Midpoint in H13. spliter. eapply l5_2. apply H10. assumption. apply midpoint_bet. assumption. assert (Bet U M C). eapply outer_transitivity_between2. apply between_symmetry. apply H12. assumption. assumption. eapply l5_2. apply H10. assumption. unfold Midpoint in H6. spliter. assumption. intro. unfold Out in *. spliter. repeat split. intro. subst U. eapply is_midpoint_id in H6. subst C'. apply H11. reflexivity. intro. subst A. apply perp_distinct in H2. spliter. apply H13. reflexivity. unfold Midpoint in H6. spliter. assert (Bet A M C'). induction H12. eapply outer_transitivity_between. apply H9. assumption. intro. apply H10. subst C. reflexivity. eapply between_inner_transitivity. apply H9. assumption. eapply l5_2. apply H11. apply between_symmetry. assumption. apply between_symmetry. assumption. assert (Perp M T A M) by (eapply perp_col2 with P Q;Col). apply perp_perp_in in H11. apply perp_in_comm in H11. eapply perp_in_per in H11. assert (Perp M T C M) 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 (M = T). apply (l8_6 C M T A). apply l8_2;auto. apply l8_2;auto. Between. subst T. split. intro. unfold Out in *. spliter. repeat split. intro. subst C. apply perp_distinct in H4. spliter. absurde. intro. subst C'. intuition. intuition. intuition. unfold Le in H. ex_and H D. assert (C <> S). intro. subst S. apply perp_distinct in H4. spliter. absurde. assert (R <> D). intro. subst D. apply cong_identity in H8. apply H9. subst S. reflexivity. assert (Perp R S A R). eapply perp_col2. apply H2. assumption. apply col_permutation_1. assumption. apply col_permutation_1. assumption. assert(exists M, Midpoint M S R /\ Midpoint M C D). unfold TS in H0. assert (~ Col A P Q). spliter. assumption. spliter. clear H0. assert (P <> Q). intro. subst Q. Col. ex_and H14 T. eapply (l8_24 S R C A D T). apply perp_sym. apply perp_left_comm. eapply perp_col2. apply H4. assumption. apply col_permutation_1. assumption. apply col_permutation_1. assumption. apply perp_right_comm. apply perp_sym. assumption. eapply col3. apply H0. apply col_permutation_1. assumption. apply col_permutation_1. assumption. apply col_permutation_1. assumption. apply between_symmetry. assumption. assumption. assumption. ex_and H12 M'. apply l7_2 in H12. assert (M = M'). eapply l7_17. apply H5. apply H12. subst M'. split. intro. unfold Out in H14. spliter. unfold Out. repeat split. assumption. apply (sym_preserve_diff U R M); auto. induction H16. assert(Bet R U D \/ Bet R D U). eapply l5_3. apply H16. assumption. induction H17. right. eapply l7_15. apply H5. apply H6. apply l7_2. apply H13. assumption. left. eapply l7_15. apply H5. apply l7_2. apply H13. apply H6. assumption. left. eapply l7_15. apply H5. apply l7_2. apply H13. apply H6. eapply between_exchange4. apply H. apply H16. unfold Out. intros. spliter. repeat split. eapply sym_preserve_diff. apply H15. apply l7_2. apply H6. apply l7_2. assumption. intro. subst R. apply perp_distinct in H11. spliter. absurde. induction H16. eapply l5_1. apply H10. eapply l7_15. apply l7_2. apply H12. apply H13. apply l7_2. apply H6. assumption. assumption. left. eapply between_exchange4. eapply l7_15. apply l7_2. apply H12. apply l7_2. apply H6. apply H13. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar