proposition: Lemma plgs_pseudo_trans : forall A B C D E F, Parallelogram_strict A B C D -> Parallelogram_strict C D E F -> Parallelogram A B F E.
proof: Proof. intros. induction(eq_dec_points A E). subst E. eapply (plgs_trans_trivial A B C D); assumption. apply plgs_diff in H. apply plgs_diff in H0. spliter. clean_duplicated_hyps. prolong D C D' D C. assert(C <> D'). intro. subst D'. apply cong_symmetry in H14. apply cong_identity in H14. subst D. tauto. assert(HH1:=plgs_par_strict A B C D H). assert(HH2:=plgs_par_strict C D E F H0). spliter. apply par_strict_symmetry in H18. assert(HH1:= l12_6 C D A B H18). assert(HH2:= l12_6 C D E F H16). assert(CongA A D D' B C D'). apply par_preserves_conga_os. left. Par. assumption. assumption. apply invert_one_side. assumption. assert(CongA E D D' F C D'). apply par_preserves_conga_os. left. Par. assumption. assumption. apply invert_one_side. assumption. assert(~ Col A C D). apply (par_strict_not_col_2 B). Par. assert(~ Col E C D). apply (par_strict_not_col_2 F). Par. induction (cop_dec C D A E). assert(HH:=cop__one_or_two_sides C D A E H24 H22 H23). assert(CongA A D E B C F). induction HH. assert(TS C D A F). apply l9_2. eapply l9_8_2. apply l9_2. apply H25. assumption. assert(TS C D B F). eapply l9_8_2. apply H26. assumption. apply(l11_22a A D E D' B C F D'). split. eapply col_two_sides. apply bet_col. apply H2. intro. subst D'. apply between_identity in H2. subst D. tauto. apply invert_two_sides. assumption. split. eapply (col_two_sides _ D). apply bet_col in H2. Col. assumption. assumption. split. assumption. apply conga_comm. assumption. apply(l11_22b A D E D' B C F D'). split. eapply col_one_side. apply bet_col. apply H2. intro. subst D'. apply between_identity in H2. subst D. tauto. apply invert_one_side. assumption. split. eapply (col_one_side _ D). apply bet_col in H2. Col. assumption. eapply one_side_transitivity. apply one_side_symmetry. apply HH1. apply one_side_symmetry. eapply one_side_transitivity. apply one_side_symmetry. apply HH2. apply one_side_symmetry. assumption. split. assumption. apply conga_comm. assumption. assert(HP0:=plgs_cong A B C D H). assert(HP1:=plgs_cong C D E F H0). spliter. apply cong_symmetry in H27. assert(HP:=cong2_conga_cong A D E B C F H25 H29 H27). assert(Par A B E F). eapply par_trans. apply par_symmetry. left. apply H18. left. assumption. induction(col_dec A E F). induction H30. apply False_ind. apply H30. exists A. split; Col. spliter. right. unfold Parallelogram_flat. repeat split; Cong. ColR. ColR. apply cong_transitivity with C D; Cong. induction(eq_dec_points A F). right. subst F. intro. subst E. apply cong_symmetry in H27. assert(HQ:=par_strict_cong_mid C A D B H17 H27). ex_and HQ M. induction H35. unfold Midpoint in *. spliter. apply H16. exists M. split; Col. unfold Midpoint in *. spliter. apply H19. exists M. split. ColR. ColR. left. assumption. assert(Par A E B F \/ ~ Par_strict D C A B \/ ~ Par_strict D C E F). eapply(cong3_par2_par ); auto. repeat split; Cong. apply par_comm. left. assumption. apply par_symmetry. left. assumption. induction H32. apply plg_to_parallelogram. apply pars_par_plg. assert(Par A B F E). eapply par_trans. apply par_symmetry. left. apply H18. apply par_right_comm. left. assumption. induction H33. assumption. spliter. apply False_ind. apply H31. Col. assumption. induction H32. apply False_ind. apply H32. apply par_strict_left_comm. assumption. apply False_ind. apply H32. apply par_strict_left_comm. assumption. destruct (par_cong_plg_2 A B E F); auto. apply par_trans with C D; Par. apply cong_transitivity with C D; apply plgs_cong_1; assumption. exfalso. assert (OS A E B F). apply (cop3_osp__os A D E); Cop. assert (~ Col D A B) by (apply (par_strict_not_col_2 C), H18). apply osp_transitivity with C. apply cop2_os__osp with A D; [|Cop..|Side]. intro; apply H24, coplanar_perm_12, coplanar_trans_1 with B; Col; Cop. apply cop2_os__osp with D E; [|Cop..|Side]. intro; apply H24, coplanar_perm_12, coplanar_trans_1 with C; Col; Cop. apply (l9_9 A E B F); [|assumption]. repeat split. apply one_side_not_col123 in H26; Col. apply one_side_not_col124 in H26; Col. apply plg_mid in H25. destruct H25 as [M []]. exists M; split; [Col|Between]. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates