proposition: Lemma plg_pseudo_trans : forall A B C D E F, Parallelogram A B C D -> Parallelogram C D E F -> Parallelogram A B F E \/ (A = B /\ C = D /\ E = F /\ A = E).
proof: Proof. intros. induction(eq_dec_points A B). subst B. induction H. unfold Parallelogram_strict in H. spliter. unfold TS in H. spliter. apply False_ind. apply H. Col. assert(C = D). assert(HH:=plgf_trivial_neq A C D H). spliter. assumption. subst D. induction H0. unfold Parallelogram_strict in H0. spliter. unfold TS in H0. spliter. apply False_ind. apply H0. Col. assert(E=F). assert(HH:=plgf_trivial_neq C E F H0). spliter. assumption. subst F. induction (eq_dec_points A E). right. repeat split; auto. left. apply plg_trivial1. assumption. assert(C <> D). intro. subst D. induction H. unfold Parallelogram_strict in H. spliter. unfold TS in H. spliter. apply H4. Col. apply plgf_sym in H. apply plgf_trivial_neq in H. spliter. contradiction. assert(E <> F). intro. subst F. induction H0. unfold Parallelogram_strict in H0. spliter. unfold TS in H0. spliter. apply H5. Col. apply plgf_sym in H0. apply plgf_trivial_neq in H0. spliter. contradiction. left. induction H; induction H0. eapply plgs_pseudo_trans. apply H. assumption. left. apply plgs_sym. apply (plgf_plgs_trans F E D C);auto. apply plgf_comm2. apply plgf_sym. assumption. apply plgs_comm2. apply plgs_sym. assumption. left. apply (plgf_plgs_trans A B C D E F); auto. right. apply (plgf_plgf_plgf A B C D E F); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates