proposition: Lemma plgf_plgs_trans : forall A B C D E F, A <> B -> Parallelogram_flat A B C D -> Parallelogram_strict C D E F -> Parallelogram_strict A B F E.
proof: Proof. intros. induction(eq_dec_points A D). subst D. induction H0. spliter. apply cong_symmetry in H4. apply cong_identity in H4. spliter. subst C. apply plgs_comm2. assumption. induction(eq_dec_points B C). subst C. induction H0. spliter. apply cong_identity in H5. spliter. subst D. apply plgs_comm2. assumption. assert(HH:=plgs_par_strict C D E F H1). spliter. assert(HH:=plgs_cong C D E F H1). spliter. assert(HH2:= l12_6 C D E F H4). assert(HOS := HH2). induction HH2. spliter. unfold TS in H9. assert(~ Col F C D). spliter. assumption. spliter. unfold TS in H8. assert(~ Col E C D). spliter. assumption. spliter. assert(D <> E). intro. subst E. apply H13. Col. assert(HH0:=H0). induction HH0. spliter. prolong D C D' D C. assert(D <> D'). intro. subst D'. apply between_identity in H22. subst D. Col. assert(C <> D'). intro. subst D'. apply cong_symmetry in H23. apply cong_identity in H23. contradiction. assert(CongA E D D' F C D'). apply(par_preserves_conga_os D E F C D'). apply par_symmetry. apply par_left_comm. left. assumption. assumption. intro. subst D'. apply cong_symmetry in H23. apply cong_identity in H23. subst D. tauto. apply invert_one_side. assumption. induction(eq_dec_points A C). subst C. assert(B=D \/ Midpoint A B D). eapply l7_20. Col. Cong. induction H27. induction H21. tauto. contradiction. unfold Parallelogram_strict. spliter. split. apply l9_2. eapply (l9_8_2 _ _ D). unfold TS. repeat split. intro. apply H10. Col. intro. apply H10. ColR. exists A. split. Col. apply midpoint_bet. apply l7_2. assumption. eapply l12_6. assumption. split. eapply (par_col_par_2 _ D). auto. unfold Midpoint in H27. spliter. apply bet_col in H27. Col. apply par_right_comm. left. assumption. apply cong_transitivity with A D; Cong. induction(eq_dec_points B D). subst D. assert(A=C \/ Midpoint B A C). eapply l7_20. Col. Cong. induction H28. tauto. apply plgs_comm2. unfold Parallelogram_strict. split. apply l9_2. eapply (l9_8_2 _ _ C). unfold TS. repeat split. auto. intro. apply H13. Col. intro. apply H13. ColR. exists B. split. Col. apply midpoint_bet. apply l7_2. assumption. eapply l12_6. apply par_strict_symmetry. assumption. split. eapply (par_col_par_2 _ C). auto. unfold Midpoint in H28. spliter. apply bet_col in H28. Col. apply par_left_comm. left. assumption. apply cong_transitivity with C B; Cong. assert(HH:=plgf_bet A B D C H0). assert(CongA A D E B C F). induction HH. spliter. eapply l11_10. apply conga_comm. apply H26. repeat split. auto. auto. eapply (l5_1 _ C). intro. subst D. Col. Between. Between. apply out_trivial. intro. subst E. apply H13. Col. repeat split. auto. auto. assert(Bet D C B). eapply outer_transitivity_between. apply H29. assumption. auto. eapply (l5_2 D); auto. intro. subst D. Col. apply out_trivial. intro. subst F. apply H10. Col. induction H29. spliter. apply (l11_10 D' D E D' C F). apply conga_comm. apply H26. repeat split;auto. left. eBetween. apply out_trivial. intro. subst E. apply H13. Col. repeat split; auto. left. eapply (bet3_cong3_bet A B C D D'); auto; Cong. apply out_trivial. intro. subst F. apply H10. Col. induction H29. spliter. eapply l11_13. apply conga_comm. apply H26. assert_diffs. apply between_symmetry. apply outer_transitivity_between with C. apply outer_transitivity_between with B. assumption. assumption. auto. assumption. auto. auto. apply between_inner_transitivity with D. Between. Between. auto. spliter. eapply l11_13. apply conga_comm. apply H26. assert_diffs. apply outer_transitivity_between with B. apply between_symmetry. apply outer_transitivity_between with C. assumption. assumption. auto. Between. auto. auto. assert_diffs. apply outer_transitivity_between with D. Between. Between. auto. auto. assert(Cong A E B F). eapply(cong2_conga_cong A D E B C F H29);Cong. assert(Cong_3 E A D F B C). repeat split; Cong. assert(Par A B E F). eapply (par_trans A B C D E F). right. repeat split; auto. intro. subst. Col. ColR. ColR. left. assumption. assert(CongA E A D F B C). apply cong3_conga. intro. subst E. apply H13. ColR. auto. assumption. assert(OS A B E F). eapply l12_6. induction H32. assumption. spliter. assert(Col A B E). ColR. apply False_ind. apply H13. eapply (col3 A B); Col. assert(Par A E F B). induction HH. prolong A B A' A B. apply (conga_to_par_os _ _ _ _ A'); auto. apply conga_comm. eapply l11_13. apply conga_comm. apply H33. apply outer_transitivity_between with B. apply between_symmetry. apply outer_transitivity_between with C. Between. Between. auto. assumption. auto. intro. subst A'. apply between_identity in H36. contradiction. apply between_symmetry. apply outer_transitivity_between with A. Between. Between. auto. intro. subst A'. apply cong_symmetry in H37. apply cong_identity in H37. contradiction. induction H35. spliter. prolong A B A' A B. apply (conga_to_par_os _ _ _ _ A'); auto. apply conga_comm. eapply l11_13. apply conga_comm. apply H33. apply outer_transitivity_between with B. apply outer_transitivity_between with C. assumption. assumption. auto. assumption. auto. intro. subst A'. apply between_identity in H37. contradiction. apply between_exchange3 with A. assumption. assumption. intro. subst A'. apply cong_symmetry in H38. apply cong_identity in H38. contradiction. induction H35. spliter. prolong A B A' A B. apply (conga_to_par_os _ _ _ _ A'); auto. apply conga_comm. eapply l11_10. apply conga_comm. apply H33. repeat split; auto. intro. subst A'. apply between_identity in H37. contradiction. right. apply between_exchange4 with B. assumption. assumption. apply out_trivial. intro. subst E. apply H13. ColR. repeat split; auto. intro. subst A'. apply cong_symmetry in H38. apply cong_identity in H38. contradiction. right. eapply (bet3_cong3_bet D _ _ A); Cong. intro. subst D. Col. apply out_trivial. intro. subst F. apply H10. ColR. spliter. prolong A B A' A C. apply (conga_to_par_os _ _ _ _ A'); auto. apply conga_comm. eapply l11_10. apply conga_comm. apply H33. repeat split; auto. intro. subst A'. apply between_identity in H37. contradiction. right. assert(Bet B C A'). eapply (bet_cong_bet A); auto. apply outer_transitivity_between with D. assumption. assumption. auto. Cong. apply between_exchange2 with B. assumption. apply between_exchange4 with C. assumption. assumption. apply out_trivial. intro. subst E. apply H13. ColR. repeat split. intro. subst A'. apply cong_symmetry in H38. apply cong_identity in H38. contradiction. auto. right. apply (bet_cong_bet A); auto. apply outer_transitivity_between with D. assumption. assumption. auto. Cong. apply out_trivial. intro. subst F. apply H10. ColR. assert(Plg A B F E). apply pars_par_plg. induction H32. apply par_strict_right_comm. assumption. spliter. apply False_ind. assert(Col A B E). ColR. apply H13. eapply (col3 A B); Col. Par. apply plg_to_parallelogram in H36. induction H36. assumption. unfold Parallelogram_flat in H36. spliter. assert(Col A B E). ColR. apply False_ind. apply H13. eapply (col3 A B); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates