proposition: Lemma triangle_par : forall A B C A' B' C', ~ Col A B C -> Par A B A' B' -> Par B C B' C' -> Par A C A' C' -> CongA A B C A' B' C'.
proof: Proof. intros. assert(HH:=midpoint_existence B B'). ex_and HH M. prolong A' M A'' A' M. prolong C' M C'' C' M. assert(Midpoint M A' A'') by (split;Cong). assert(Midpoint M C' C'') by (split;Cong). assert(A' <> B'). intro. subst A'. apply par_distincts in H0. spliter. tauto. assert(C' <> B'). intro. subst C'. apply par_distincts in H1. spliter. tauto. assert(Par B' C' B C''). apply (l12_17 _ _ _ _ M); Midpoint. assert(Col B B C /\ Col C'' B C). apply(parallel_uniqueness B' C' B C B C'' B); Col. Par. assert(Par B' A' B A''). apply (l12_17 _ _ _ _ M); Midpoint. assert(Col B B A /\ Col A'' B A). apply(parallel_uniqueness B' A' B A B A'' B); Col. apply par_symmetry. apply par_comm. assumption. spliter. clear H13. clear H15. assert(CongA A' B' C' A'' B C''). apply (symmetry_preserves_conga _ _ _ _ _ _ M); Midpoint. eapply conga_trans; [|apply conga_sym, H13]. show_distinct B A''. assert_diffs;intuition. show_distinct B C''. assert_diffs;intuition. assert(A <> B). apply par_distincts in H0. tauto. assert(B <> C). apply par_distincts in H1. tauto. assert(Par A C A'' C''). eapply par_trans. apply H2. eapply (l12_17 _ _ _ _ M); Midpoint. intro. subst C'. apply par_distincts in H2. tauto. apply par_distincts in H21. spliter. induction H17. assert(Par_strict A C A'' C''). induction H21. assumption. spliter. apply False_ind. apply H. assert(C <> C''). intro. subst C''. apply between_identity in H17. subst C. tauto. assert(Col A C C''). ColR. apply bet_col in H17. apply (col3 C C''); Col. induction H16. apply(l11_14 A B C A'' C''); Between. apply False_ind. induction (eq_dec_points A A''). subst A''. apply H24. exists A. split; Col. induction H16. assert(TS A C A'' B). repeat split; Col. intro. apply H. apply bet_col in H16. apply bet_col in H17. eapply (col3 A A''); Col. exists A. split; Col. Between. assert(OS A C B C''). eapply (out_one_side_1 _ _ _ _ C); Col. unfold Out. repeat split; auto. intro. subst C''. apply between_identity in H17. subst C. tauto. left. Between. assert(TS A C A'' C''). apply l9_2. eapply l9_8_2. apply l9_2. apply H26. assumption. unfold TS in H28. spliter. ex_and H30 T. apply H24. exists T. apply bet_col in H31. split; Col. assert(TS A'' C'' A B). repeat split; Col. intro. apply H. apply bet_col in H16. apply bet_col in H17. assert(Col A'' C'' B). ColR. assert(Col A'' C'' C). ColR. eapply (col3 A'' C''); Col. intro. apply bet_col in H16. apply bet_col in H17. apply H. assert(Col B C A''). ColR. apply (col3 B A''); Col. exists A''. split; Col. assert(OS A'' C'' B C). apply out_one_side_1 with C''; Col. intro. apply H. apply bet_col in H16. apply bet_col in H17. assert(Col A'' B C). ColR. apply (col3 A'' B); Col. repeat split; auto. intro. subst. unfold Par_strict in H24. spliter. apply H27. exists C''; split; Col. assert(TS A'' C'' A C). apply l9_2. eapply l9_8_2. apply l9_2. apply H26. assumption. unfold TS in H28. spliter. ex_and H30 T. apply H24. exists T. apply bet_col in H31. split; Col. induction H17. induction H16. assert(Par_strict A C A'' C''). induction H21. assumption. spliter. apply False_ind. apply H. assert(A <> A''). intro. subst A''. apply between_identity in H16. contradiction. assert(Col C A A''). ColR. apply bet_col in H16. apply (col3 A A''); Col. apply False_ind. induction (eq_dec_points C C''). subst C''. apply H24. exists C. split; Col. assert(TS A C C'' B). repeat split; Col. intro. apply H. apply bet_col in H16. apply bet_col in H17. eapply (col3 C C''); Col. exists C. split; Col. Between. assert(OS A C B A''). eapply (out_one_side _ _ _ _); Col. unfold Out. repeat split; auto. intro. subst A''. apply between_identity in H16. contradiction. left. Between. assert(TS A C A'' C''). eapply l9_8_2. apply l9_2. apply H26. assumption. unfold TS in H28. spliter. ex_and H30 T. apply H24. exists T. apply bet_col in H31. split; Col. induction H16. apply out2__conga. repeat split; auto. repeat split; auto. apply out2__conga. repeat split; auto. left. Between. repeat split; auto. induction H16. assert(Par_strict A C A'' C''). induction H21. assumption. spliter. apply False_ind. apply H. assert(A <> A''). intro. subst A''. apply between_identity in H16. contradiction. assert(Col C A A''). ColR. apply bet_col in H16. apply (col3 A A''); Col. apply False_ind. induction (eq_dec_points C C''). subst C''. apply H24. exists C. split; Col. assert(TS A'' C'' C B). repeat split; Col. intro. apply H. apply bet_col in H16. apply bet_col in H17. assert(Col A'' C'' B). ColR. assert(Col A'' C'' A). ColR. eapply (col3 A'' C''); Col. intro. apply bet_col in H16. apply bet_col in H17. apply H. assert(Col B C A''). ColR. apply (col3 B A''); Col. exists C''. split; Col. assert(OS A'' C'' B A). apply out_one_side. left. intro. apply H. apply bet_col in H16. apply bet_col in H17. assert(Col C B A''). ColR. apply (col3 A'' B); Col. repeat split; auto. intro. subst. unfold Par_strict in H24. spliter. apply H27. exists A''. split; Col. assert(TS A'' C'' A C). eapply l9_8_2. apply l9_2. apply H26. assumption. unfold TS in H28. spliter. ex_and H30 T. apply H24. exists T. apply bet_col in H31. split; Col. induction H16. apply out2__conga. repeat split; auto. repeat split; auto. left. Between. apply out2__conga. repeat split; auto. left. Between. repeat split; auto. left. Between. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors