proposition: Lemma l10_16 : forall A B C A' B' P, ~ Col A B C -> ~ Col A' B' P -> Cong A B A' B' -> exists C', Cong_3 A B C A' B' C' /\ OS A' B' P C' .
proof: Proof. intros. induction (eq_dec_points A B). subst B. apply cong_symmetry in H1. apply False_ind. apply H. apply col_trivial_1. assert(exists X, Col A B X /\ Perp A B C X). apply l8_18_existence. assumption. ex_and H3 X. assert (exists X', Cong_3 A B X A' B' X'). eapply l4_14. assumption. assumption. ex_elim H5 X'. assert (exists Q, Perp A' B' Q X' /\ OS A' B' P Q). apply l10_15. eapply l4_13. apply H3. assumption. assumption. ex_and H5 Q. assert (exists C', Out X' C' Q /\ Cong X' C' X C). eapply l6_11_existence. apply perp_distinct in H5. spliter. assumption. intro. subst C. apply perp_distinct in H4. spliter. absurde. ex_and H8 C'. exists C'. unfold Cong_3 in *. spliter. assert (Cong A C A' C'). induction(eq_dec_points A X). subst X. apply cong_symmetry in H10. apply cong_identity in H10. subst X'. apply cong_symmetry. assumption. apply l10_12 with X X'. apply perp_in_per. eapply l8_14_2_1b_bis. eapply perp_col. assumption. apply perp_right_comm. apply H4. assumption. apply col_trivial_3. apply col_trivial_1. apply perp_in_per. eapply l8_14_2_1b_bis. eapply perp_col. intro assumption. subst X'. apply cong_identity in H10. contradiction. apply perp_sym. eapply perp_col. intro. subst X'. apply cong_symmetry in H9. apply cong_identity in H9. subst X. apply perp_distinct in H4. spliter. absurde. apply perp_sym. apply perp_right_comm. apply H5. apply col_permutation_5. eapply out_col. assumption. eapply l4_13. apply H3. unfold Cong_3. repeat split;assumption. apply col_trivial_3. apply col_trivial_1. assumption. apply cong_symmetry. assumption. assert (Cong B C B' C'). induction(eq_dec_points B X). subst X. apply cong_symmetry in H11. apply cong_identity in H11. subst X'. apply cong_symmetry. assumption. apply l10_12 with X X'. apply perp_in_per. eapply l8_14_2_1b_bis. eapply perp_col. assumption. apply perp_comm. apply H4. apply col_permutation_4. assumption. apply col_trivial_3. apply col_trivial_1. apply perp_in_per. eapply l8_14_2_1b_bis. eapply perp_col. intro assumption. subst X'. apply cong_identity in H11. contradiction. apply perp_sym. eapply perp_col. intro. subst X'. apply cong_symmetry in H9. apply cong_identity in H9. subst X. apply perp_distinct in H4. spliter. absurde. apply perp_sym. apply perp_comm. apply H5. apply col_permutation_5. eapply out_col. assumption. apply col_permutation_4. eapply l4_13. apply H3. unfold Cong_3. repeat split; assumption. apply col_trivial_3. apply col_trivial_1. assumption. apply cong_symmetry. assumption. repeat split. assumption. assumption. assumption. assert (T19 := (l9_19 A' B' C' Q X')). assert (OS A' B' C' Q <-> Out X' C' Q /\ ~ Col A' B' C'). apply T19. eapply l4_13. apply H3. unfold Cong_3. repeat split; assumption. apply col_permutation_1. apply out_col. assumption. apply cong_symmetry in H1. destruct H14. spliter. assert (OS A' B' C' Q). apply H15. split. assumption. intro. apply H. eapply l4_13. apply H16. unfold Cong_3. repeat split. assumption. apply cong_symmetry. assumption. apply cong_symmetry. assumption. eapply one_side_transitivity. apply H7. apply one_side_symmetry. assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity