proposition: Lemma l13_14 : forall O A B C O' A' B' C', Par_strict O A O' A' -> Col O A B -> Col O B C -> Col O A C -> Col O' A' B' -> Col O' B' C' -> Col O' A' C' -> Par A C' A' C -> Par B C' B' C -> Par A B' A' B.
proof: Proof. intros. assert(HP:= H). unfold Par_strict in HP. spliter. assert (O <> A) by (apply par_strict_distinct in H; spliter; auto). assert (O' <> A') by (apply par_strict_distinct in H; spliter; auto). assert(~Col O A A'). intro. apply H9. exists A'. split; Col. induction(eq_dec_points A C). subst C. induction H6. apply False_ind. apply H6. exists A. split; Col. spliter. assert(A' = C'). eapply (l6_21 A C' O' A'); Col. intro. apply H9. exists A. split. Col. eapply (col_transitivity_1 _ C'). intro. subst C'. apply H9. exists A. Col. Col. Col. subst C'. Par. assert(A' <> C'). intro. subst C'. induction H6. apply H6. exists A'. split; Col. spliter. apply H13. eapply (l6_21 A A' O A); Col. assert(Par_strict A C A' C'). split. Cop. intro. apply H9. ex_and H15 X. exists X. split. ColR. ColR. assert(Plg A C A' C'). apply(pars_par_plg A C A' C'). auto. apply par_right_comm. auto. induction(eq_dec_points B C). subst C. assert(B' = C'). eapply (l6_21 B C' A' C'). intro. apply H9. exists B. split. Col. ColR. auto. induction H7. apply False_ind. apply H7. exists B. split; Col. spliter. Col. Col. ColR. Col. subst. Par. assert(B' <> C'). intro. subst C'. induction H7. apply H7. exists B'. split; Col. spliter. apply H17. eapply (l6_21 A C B' B). intro. induction H6. apply H6. exists C. split; Col. spliter. apply H15. exists B'. split; Col. auto. ColR. Col. Col. Col. assert(Par_strict B C B' C'). split. Cop. intro. apply H9. ex_and H19 X. exists X. split. assert(Col X O B). ColR. induction(eq_dec_points O B). subst O. ColR. ColR. assert(Col X O' B'). ColR. induction(eq_dec_points O' B'). subst O'. ColR. ColR. assert(Plg B C B' C'). apply(pars_par_plg B C B' C'). auto. apply par_right_comm. auto. assert(Parallelogram A C A' C'). apply plg_to_parallelogram. auto. assert(Parallelogram B C B' C'). apply plg_to_parallelogram. auto. apply plg_mid in H21. apply plg_mid in H22. ex_and H21 M. ex_and H22 N. assert(M = N). eapply (l7_17 C C'); auto. subst N. assert(Parallelogram A B A' B'). apply(mid_plg A B A' B' M). left. intro. subst A'. apply H12. Col. assumption. assumption. apply par_right_comm. induction(eq_dec_points A B). subst B. assert(B' = A'). eapply (symmetric_point_uniqueness A M); auto. subst B'. apply par_reflexivity. intro. subst A'. apply H12. Col. apply plg_par; auto. intro. subst A'. apply H9. exists B. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project