proposition: Lemma l13_10_aux1 : forall O A B P Q la lb lp lq, Col O A B -> Col O P Q -> Perp O P P A -> Perp O Q Q B -> Q_Cong la -> Q_Cong lb -> Q_Cong lp -> Q_Cong lq -> la O A -> lb O B -> lp O P -> lq O Q -> exists a, Q_CongA_Acute a /\ Lcos lp la a /\ Lcos lq lb a.
proof: Proof. intros. assert(Acute A O P). apply (perp_acute _ _ P); Col; Perp. assert(P <> O). intro. subst P. apply perp_not_eq_1 in H1. tauto. assert(A <> O). intro. subst A. apply perp_not_col in H1. apply H1. Col. assert(Q <> O). intro. subst Q. apply perp_not_eq_1 in H2. tauto. assert(B <> O). intro. subst B. apply perp_not_col in H2. apply H2. Col. assert(HH:= anga_exists A O P H13 H12 H11). ex_and HH a. assert(a B O Q). assert(~ Par O P A P). intro. unfold Par in H18. induction H18. unfold Par_strict in H18. spliter. apply H19. exists P. split; Col. spliter. apply perp_comm in H1. apply perp_not_col in H1. apply H1. Col. assert(A <> P). apply perp_not_eq_2 in H1. auto. assert(Proj O O O P A P). unfold Proj. repeat split; Col. assert(Proj A P O P A P). unfold Proj. repeat split; Col. left. apply par_reflexivity. auto. assert(Proj B Q O P A P). unfold Proj. repeat split; Col. left. apply (l12_9 _ _ _ _ O P); Cop. apply perp_sym. eapply (perp_col _ Q); Col. Perp. Perp. induction H. assert(Bet O P Q). apply(per23_preserves_bet O A B P Q); auto. apply perp_in_per. apply perp_comm in H1. apply perp_perp_in in H1. Perp. apply perp_in_per. apply perp_comm in H2. apply perp_perp_in in H2. Perp. assert(CongA A O P B O Q). apply out2__conga. repeat split; auto. repeat split; auto. apply (anga_conga_anga _ A O P); auto. induction H. assert(Bet P Q O). apply between_symmetry. apply(per23_preserves_bet O B A Q P); Between. Col. apply perp_in_per. apply perp_comm in H2. apply perp_perp_in in H2. Perp. apply perp_comm in H1. apply perp_perp_in in H1. Perp. assert(CongA A O P B O Q). apply out2__conga. repeat split; auto. left. Between. repeat split; auto. left. Between. apply (anga_conga_anga _ A O P); auto. assert(Bet Q O P). apply(per13_preserves_bet B O A Q P); auto. Col. apply perp_in_per. apply perp_comm in H2. apply perp_perp_in in H2. Perp. apply perp_comm in H1. apply perp_perp_in in H1. Perp. assert(CongA A O P B O Q). eapply (l11_14 ); Between. apply (anga_conga_anga _ A O P); auto. exists a. repeat split; auto. exists O. exists P. exists A. repeat split; auto. apply perp_in_per. Perp. apply anga_sym; auto. exists O. exists Q. exists B. repeat split; auto. apply perp_in_per. Perp. apply anga_sym; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project