proposition: Lemma angle_construction_1 : forall A B C A' B' P, ~ Col A B C -> ~ Col A' B' P -> exists C', CongA A B C A' B' C' /\ OS A' B' C' P.
proof: Proof. intros. assert (exists C0, Col B A C0 /\ Perp B A C C0). eapply l8_18_existence. intro. apply H. apply col_permutation_4. assumption. ex_and H1 C0. induction(eq_dec_points B C0). subst C0. assert (exists C', Per C' B' A' /\ Cong C' B' C B /\ OS A' B' C' P). apply ex_per_cong. intro. subst A'. apply H0. apply col_trivial_1. intro. subst C. apply H. apply col_trivial_2. apply col_trivial_2. assumption. ex_and H3 C'. exists C'. split. eapply l11_16. apply perp_perp_in in H2. apply perp_in_comm in H2. apply perp_in_per in H2. assumption. intro. subst A. apply H. apply col_trivial_1. intro. subst C. apply H. apply col_trivial_2. apply l8_2. assumption. intro. subst A'. apply H0. apply col_trivial_1. intro. subst C'. apply cong_symmetry in H4. apply cong_identity in H4. subst C. apply H. apply col_trivial_2. assumption. induction (out_dec B A C0). assert (exists C0', Out B' A' C0' /\ Cong B' C0' B C0). eapply segment_construction_3. intro. subst A'. apply H0. apply col_trivial_1. assert (Perp_at C0 C0 C B C0). eapply perp_perp_in. apply perp_sym. eapply perp_col. assumption. apply perp_right_comm. apply H2. assumption. assumption. ex_and H5 C0'. assert (exists C' , Per C' C0' B' /\ Cong C' C0' C C0 /\ OS B' C0' C' P). apply ex_per_cong. intro. subst C0'. unfold Out in H5. spliter. absurde. intro. subst C0. unfold Perp in H2. ex_and H2 X. unfold Perp_at in H7. spliter. absurde. apply col_trivial_2. intro. apply H0. apply col_permutation_2. eapply (col_transitivity_1 _ C0'). intro. subst C0'. unfold Out in H5. spliter. absurde. assumption. apply out_col. apply l6_6. assumption. ex_and H7 C'. assert (Cong_3 C0 B C C0' B' C'). unfold Cong_3. repeat split. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. apply cong_commutativity. assumption. eapply (l10_12 _ C0). assert(Perp B C0 C C0 ). eapply perp_col. intro. subst C0. apply perp_distinct in H2. spliter. absurde. apply H2. assumption. apply perp_left_comm in H10. apply perp_perp_in in H10. apply perp_in_per. apply perp_in_comm. assumption. apply l8_2. apply H7. apply cong_symmetry. assumption. apply cong_symmetry. apply cong_commutativity. assumption. exists C'. split. apply l11_10 with C0 C C0' C'. apply cong3_conga. intro. subst C0. absurde. intro. subst C. apply H. apply col_trivial_2. assumption. assumption. apply out_trivial. intro. subst C. apply H. apply col_trivial_2. assumption. apply out_trivial. intro. subst C'. apply l8_8 in H7. subst C0'. unfold Out in H5. spliter. absurde. apply invert_one_side. apply col_one_side with C0'. apply out_col. apply l6_6. assumption. intro. subst A'. apply H0. apply col_trivial_1. assumption. apply not_out_bet in H4. prolong A' B' C0' B C0. assert (exists C' , Per C' C0' B' /\ Cong C' C0' C C0 /\ OS B' C0' C' P). apply ex_per_cong. intro. subst C0'. apply cong_symmetry in H6. apply cong_identity in H6. subst C0. absurde. intro. subst C0. apply perp_distinct in H2. spliter. absurde. apply col_trivial_2. intro. apply H0. apply col_permutation_2. eapply col_transitivity_1 with C0'. intro. treat_equalities. absurde. assumption. unfold Col. right; right. assumption. ex_and H7 C'. exists C'. split. assert (Cong_3 C0 B C C0' B' C'). repeat split. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply cong_commutativity. apply (l10_12 _ C0 _ _ C0'). assert(Perp B C0 C C0 ). eapply perp_col. intro. subst C0. apply perp_distinct in H2. spliter. absurde. apply H2. assumption. apply perp_left_comm in H10. apply perp_perp_in in H10. apply perp_in_per. apply perp_in_sym. assumption. assumption. apply cong_symmetry. assumption. apply cong_symmetry. apply cong_commutativity. assumption. apply l11_13 with C0 C0'. apply cong3_conga; auto. intro. subst C. apply H. apply col_trivial_2. apply between_symmetry. assumption. intro. subst A. apply H. apply col_trivial_1. apply between_symmetry. assumption. intro. subst A'. apply H0. apply col_trivial_1. apply invert_one_side. apply col_one_side with C0'. unfold Col. right; right. assumption. intro. subst A'. apply H0. apply col_trivial_1. assumption. apply col_permutation_4. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2