proposition: Lemma l13_10 : forall A B C A' B' C' O, ~ Col O A A' -> B <> O -> C <> O -> Col O A B -> Col O B C -> B' <> O -> C' <> O -> Col O A' B' -> Col O B' C' -> Perp2 B C' C B' O -> Perp2 C A' A C' O -> Perp2 A B' B A' O.
proof: Proof. intros. assert(HH8:= H8). assert(HH9:= H9). assert(Col O A C). apply (col_transitivity_1 _ B); Col. assert(Col O A' C'). apply (col_transitivity_1 _ B'); Col. assert(A <> O). intro. subst A. apply H. Col. assert(~ Col A B' O). intro. apply H. apply (col_transitivity_1 _ B'); Col. apply perp2_perp_in in HH8. ex_and HH8 L. ex_and H14 L'. apply perp2_perp_in in HH9. ex_and HH9 M. ex_and H19 M'. assert(HH:=l8_18_existence A B' O H13). ex_and HH N. unfold Perp2. exists O. exists N. repeat split. Col. Perp. assert(HH:=lg_exists O A). ex_and HH la. assert(HH:=lg_exists O B). ex_and HH lb. assert(HH:=lg_exists O C). ex_and HH lc. assert(HH:=lg_exists O A'). ex_and HH la'. assert(HH:=lg_exists O B'). ex_and HH lb'. assert(HH:=lg_exists O C'). ex_and HH lc'. assert(HH:=lg_exists O L). ex_and HH ll. assert(HH:=lg_exists O L'). ex_and HH ll'. assert(HH:=lg_exists O M). ex_and HH lm. assert(HH:=lg_exists O M'). ex_and HH lm'. assert(HH:=lg_exists O N). ex_and HH ln. assert(O <> L). apply perp_in_perp_bis in H17. induction H17. apply perp_not_eq_1 in H17. tauto. apply perp_not_eq_1 in H17. auto. assert(O <> L'). apply perp_in_perp_bis in H18. induction H18. apply perp_not_eq_1 in H18. tauto. apply perp_not_eq_1 in H18. auto. assert(~ Col O B B'). intro. apply H. assert(Col O A B'). eapply (col_transitivity_1 _ B); Col. eapply (col_transitivity_1 _ B'); Col. assert(~ Col O C C'). intro. apply H. assert(Col O A C'). eapply (col_transitivity_1 _ C); Col. eapply (col_transitivity_1 _ C'); Col. assert(exists a, Q_CongA_Acute a /\ Lcos ll lb a /\ Lcos ll' lc a). induction(eq_dec_points B L). subst L. assert(C = L'). eapply (l6_21 O B B' L'); Col. intro. subst L'. contradiction. subst L'. apply (l13_10_aux2 O B C); Col. apply (l13_10_aux1 O B C L L'); Col. apply perp_in_perp_bis in H17. induction H17. apply perp_not_eq_1 in H17. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ C');auto. Perp. apply perp_in_perp_bis in H18. induction H18. apply perp_not_eq_1 in H18. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ B'); auto. intro. subst L'. assert(Col O B L). eapply (col_transitivity_1 _ C); Col. apply H52. apply(l6_21 O C C' B B L); Col. intro. subst C'. unfold Perp_at in H17. tauto. Perp. ex_and H52 l'. assert(exists a, Q_CongA_Acute a /\ Lcos ll lc' a /\ Lcos ll' lb' a). induction(eq_dec_points C' L). subst L. assert(B' = L'). eapply (l6_21 O C' C L'); Col. intro. subst L'. apply H51. Col. subst L'. eapply (l13_10_aux2 O C' B'); Col. apply (l13_10_aux1 O C' B' L L'); Col. apply perp_in_perp_bis in H17. induction H17. apply perp_not_eq_1 in H17. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ B); Col. Perp. apply perp_in_perp_bis in H18. induction H18. apply perp_not_eq_1 in H18. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ C);Col. intro. subst L'. assert(Col O C' L). eapply (col_transitivity_1 _ B'); Col. apply H55. apply(l6_21 O B' B C' C' L); Col. intro. subst C'. unfold Perp_at in H17. tauto. Perp. ex_and H55 l. assert(exists a, Q_CongA_Acute a /\ Lcos lm lc a /\ Lcos lm' la a). induction (eq_dec_points C M). subst M. assert(A = M'). eapply (l6_21 O C C' M'); Col. intro. subst M'. contradiction. subst M'. apply (l13_10_aux2 O C A); Col. apply (l13_10_aux1 O C A M M'); Col. apply perp_in_perp_bis in H22. induction H22. apply perp_not_eq_1 in H22. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ A');auto. Perp. apply perp_in_perp_bis in H23. induction H23. apply perp_not_eq_1 in H23. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ C'); auto. intro. subst M'. assert(Col O C M). eapply (col_transitivity_1 _ A); Col. apply H58. apply(l6_21 O A A' C C M); Col. intro. subst A'. unfold Perp_at in H22. tauto. Perp. ex_and H58 m'. assert(exists a, Q_CongA_Acute a /\ Lcos lm la' a /\ Lcos lm' lc' a). induction(eq_dec_points A' M). subst M. assert(C' = M'). eapply (l6_21 O A' A M'); Col. intro. subst M'. apply H. Col. subst M'. eapply (l13_10_aux2 O A' C'); Col. intro. subst A'. apply H. Col. apply (l13_10_aux1 O A' C' M M'); Col. apply perp_in_perp_bis in H22. induction H22. apply perp_not_eq_1 in H22. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ C);Col. Perp. apply perp_in_perp_bis in H23. induction H23. apply perp_not_eq_1 in H23. tauto. apply perp_sym. apply perp_comm. eapply (perp_col _ A);Col. intro. subst M'. assert(Col O A' M). eapply (col_transitivity_1 _ C'); Col. apply H61. apply(l6_21 O C' C A' A' M); Col. intro. subst A'. unfold Perp_at in H22. tauto. Perp. ex_and H61 m. assert(exists a, Q_CongA_Acute a /\ Lcos ln la a). assert(exists a, Q_CongA_Acute a /\ a A O N). apply(anga_exists A O N). intro. subst A. apply H. Col. apply perp_not_eq_2 in H25. auto. induction(eq_dec_points A N). subst N. apply acute_trivial. intro. subst A. apply H. Col. eapply (perp_acute _ _ N). Col. apply perp_in_left_comm. apply perp_perp_in. apply perp_sym. apply (perp_col _ B'). auto. Perp. Col. ex_and H64 n'. exists n'. split. auto. unfold Lcos. repeat split; auto. exists O. exists N. exists A. repeat split; auto. induction(eq_dec_points A N). subst N. apply l8_2. apply l8_5. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_left_comm. apply (perp_col _ B'). auto. Perp. Col. apply anga_sym; auto. ex_and H64 n'. assert(exists a, Q_CongA_Acute a /\ Lcos ln lb' a). assert(exists a, Q_CongA_Acute a /\ a B' O N). apply(anga_exists B' O N). intro. subst B'. apply H50. Col. apply perp_not_eq_2 in H25. auto. induction(eq_dec_points B' N). subst N. apply acute_trivial. auto. eapply (perp_acute _ _ N). Col. apply perp_in_left_comm. apply perp_perp_in. apply perp_sym. apply (perp_col _ A). auto. Perp. Col. ex_and H66 n. exists n. split. auto. unfold Lcos. repeat split; auto. exists O. exists N. exists B'. repeat split; auto. induction(eq_dec_points B' N). subst N. apply l8_2. apply l8_5. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_left_comm. apply (perp_col _ A). auto. Perp. Col. apply anga_sym; auto. ex_and H66 n. assert(Eq_Lcos lc l' lb' l). unfold Eq_Lcos. exists ll'. split; auto. assert(Eq_Lcos lb l' lc' l). unfold Eq_Lcos. exists ll. split; auto. assert(Eq_Lcos lc m' la' m). unfold Eq_Lcos. exists lm. split; auto. assert(Eq_Lcos la m' lc' m). unfold Eq_Lcos. exists lm'. split; auto. assert(Eq_Lcos la n' lb' n). unfold Eq_Lcos. exists ln. split; auto. assert(exists lp, Lcos lp lb n'). apply(lcos_exists lb n'); auto. intro. unfold Q_Cong_Null in H73. spliter. ex_and H74 X. apply H0. eapply (cong_identity _ _ X). apply (lg_cong lb); auto. apply (lg_sym lb); auto. ex_and H73 bn'. assert(exists lp, Lcos lp ll n'). apply(lcos_exists ll n'); auto. intro. unfold Q_Cong_Null in H73. spliter. ex_and H75 X. apply H48. apply (cong_identity _ _ X). apply (lg_cong ll); auto. ex_and H73 bl'n'. assert(exists lp, Lcos lp bn' l'). apply(lcos_exists bn' l'); auto. apply lcos_lg_anga in H74. spliter. auto. assert(HH:= lcos_lg_not_null bn' lb n' H74 ). tauto. ex_and H73 bn'l'. assert(Lcos2 bl'n' lb l' n'). unfold Lcos2. exists ll. split; auto. assert(Lcos2 bn'l' lb n' l'). unfold Lcos2. exists bn'. split; auto. assert(EqL bl'n' bn'l'). apply lcos2_comm in H77. apply (lcos2_uniqueness lb _ _ l' n'); auto. apply lcos_lg_anga in H75. apply lcos_lg_anga in H76. spliter. assert(Eq_Lcos2 lb l' n' lb n' l'). unfold Eq_Lcos2. exists bl'n'. split; auto. eapply (lcos2_eql_lcos2 lb _ bn'l'). auto. reflexivity. symmetry; auto. assert(Eq_Lcos2 lb l' n' lc' l n'). apply lcos_eq_lcos2_eq; auto. assert(Eq_Lcos3 lb l' n' m lc' l n' m). apply lcos2_eq_lcos3_eq; auto. assert(Eq_Lcos3 lb l' n' m lc' m l n'). unfold Eq_Lcos3 in H87. ex_and H87 lp. unfold Eq_Lcos3. exists lp. split; auto. apply lcos3_permut1. apply lcos3_permut2. auto. assert(Eq_Lcos3 la m' l n' lc' m l n'). apply lcos_eq_lcos3_eq; auto. assert(Eq_Lcos3 lb l' n' m la m' l n'). apply (lcos3_eq_trans _ _ _ _ lc' m l n'); auto. apply lcos3_eq_sym; auto. assert(Eq_Lcos3 lb l' n' m la n' m' l). unfold Eq_Lcos3 in H90. ex_and H90 lp. unfold Eq_Lcos3. exists lp. split; auto. apply lcos3_permut1. apply lcos3_permut2. auto. assert(Eq_Lcos3 la n' m' l lb' n m' l). apply lcos_eq_lcos3_eq; auto. assert(Eq_Lcos3 lb l' n' m lb' n m' l). apply (lcos3_eq_trans _ _ _ _ la n' m' l); auto. assert(Eq_Lcos3 lb l' n' m lb' l n m'). unfold Eq_Lcos3 in H93. ex_and H93 lp. unfold Eq_Lcos3. exists lp. split; auto. apply lcos3_permut1. apply lcos3_permut2. auto. assert(Eq_Lcos3 lb' l n m' lc l' n m'). apply lcos_eq_lcos3_eq; auto. apply lcos_eq_sym; auto. assert(Eq_Lcos3 lb l' n' m lc l' n m'). apply (lcos3_eq_trans _ _ _ _ lb' l n m'); auto. assert(Eq_Lcos3 lb l' n' m lc m' l' n). unfold Eq_Lcos3 in H96. ex_and H96 lp. unfold Eq_Lcos3. exists lp. split; auto. apply lcos3_permut1. apply lcos3_permut2. auto. assert(Eq_Lcos3 la' m l' n lc m' l' n). apply lcos_eq_lcos3_eq; auto. apply lcos_eq_sym; auto. assert(Eq_Lcos3 lb l' n' m la' m l' n). apply (lcos3_eq_trans _ _ _ _ lc m' l' n); auto. apply lcos3_eq_sym; auto. assert(Eq_Lcos3 lb l' n' m la' n l' m). unfold Eq_Lcos3 in H99. ex_and H99 lp. unfold Eq_Lcos3. exists lp. split; auto. apply lcos3_permut2. auto. assert(Eq_Lcos2 lb l' n' la' n l'). apply (lcos3_lcos2 _ _ _ _ _ _ m); auto. assert(Eq_Lcos2 lb n' l' la' n l'). unfold Eq_Lcos2 in H101. ex_and H101 lp. unfold Eq_Lcos2. exists lp. split; auto. apply lcos2_comm. auto. assert(Eq_Lcos lb n' la' n). apply (lcos2_lcos) in H102. auto. clear H85 H86 H87 H88 H89 H90 H91 H92 H93 H94 H95 H96 H97 H98 H99 H100 H101 H102. unfold Eq_Lcos in H103. ex_and H103 ln'. assert(O <> N). apply perp_not_eq_2 in H25; auto. apply lcos_lg_anga in H85. spliter. assert(n' A O N). apply(lcos_per_anga _ _ _ la ln); auto. induction(eq_dec_points A N). subst N. apply l8_2. apply l8_5. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_left_comm. apply (perp_col _ B'); Col. assert(n B' O N). apply(lcos_per_anga _ _ _ lb' ln); auto. induction(eq_dec_points B' N). subst N. apply l8_2. apply l8_5. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_left_comm. apply (perp_col _ A); Col. Perp. assert(Bet A O B \/ Out O A B \/ ~ Col A O B). apply(or_bet_out A O B); auto. induction H93. assert(HH:=ex_point_lg_bet ln' N O H89). ex_and HH N'. assert(O <> N'). intro. subst N'. assert(HH:=lcos_lg_not_null ln' lb n' H85). spliter. apply H96. unfold Q_Cong_Null. split; auto. exists O. auto. assert(A' <> B). intro. subst A'. contradiction. assert(Per O N' B). apply(lcos_per O N' B ln' lb n'); auto. assert(CongA N O A B O N'). apply(l11_13 N' O A A O N' N B ); Between. apply conga_left_comm. apply conga_refl; auto. apply (anga_conga_anga n' A O N); auto. apply conga_comm. auto. assert(Per O N' A'). apply(lcos_per O N' A' ln' la' n); auto. assert(CongA N O B' A' O N'). apply(l11_13 N' O B' B' O N' N A' ); Between. apply conga_left_comm. apply conga_refl; auto. apply between_symmetry. apply(l13_10_aux3 A B C A' B' C' O); auto. intro. subst A'. apply H. Col. eapply (anga_conga_anga n B' O N); auto. apply conga_comm. auto. apply (perp_col _ N'); Col. apply cop_per2__perp; auto. induction(eq_dec_points N' B). right. subst N'. auto. left. auto. apply coplanar_perm_16. apply col_cop__cop with N; Col. apply coplanar_perm_5. apply col_cop__cop with B'; Col. exists A. right. left. split; Col. induction H93. assert(exists N' : Tpoint, ln' O N' /\ Out O N' N). apply(ex_point_lg_out ln' O N H87 H89). assert(HH:=lcos_lg_not_null ln' la' n H86). spliter. auto. ex_and H94 N'. assert(Per O N' B). apply(lcos_per O N' B ln' lb n'); auto. assert(CongA A O N B O N'). apply out2__conga; auto. apply l6_6. auto. apply (anga_conga_anga n' A O N); auto. apply conga_right_comm. auto. assert(Per O N' A'). apply(lcos_per O N' A' ln' la' n); auto. assert(CongA B' O N A' O N'). apply out2__conga; auto. apply (l13_10_aux5 A B C A' B' C'); Col. apply (anga_conga_anga n B' O N); auto. apply conga_right_comm. auto. apply(perp_col _ N'). auto. apply (cop_per2__perp); auto. intro. subst N'. unfold Out in H95. tauto. intro. subst A'. contradiction. induction(eq_dec_points N' B). subst N'. right. intro. subst A'. contradiction. left. auto. apply coplanar_perm_16. apply col_cop__cop with N; Col. apply coplanar_perm_5. apply col_cop__cop with B'; Col. exists A. right. left. split; Col. apply out_col in H95. Col. apply False_ind. apply H93. Col. split; intro; apply H; ColR. split; intro; apply H; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project