proposition: Lemma plgf_plgf_plgf: forall A B C D E F, A <> B -> Parallelogram_flat A B C D -> Parallelogram_flat C D E F -> Parallelogram_flat A B F E.
proof: Proof. intros. assert(C <> D). unfold Parallelogram_flat in H0. spliter. intro. subst D. apply cong_identity in H3. contradiction. assert(E <> F). unfold Parallelogram_flat in H1. spliter. intro. subst F. apply cong_identity in H4. contradiction. assert(HH:=plgs_existence C D H2). ex_and HH D'. ex_and H4 C'. assert(Parallelogram_strict A B C' D'). eapply (plgf_plgs_trans A B C D); auto. assert(Parallelogram_strict E F C' D'). eapply (plgf_plgs_trans E F C D); auto. apply plgf_sym. assumption. assert(Parallelogram A B F E). eapply plgs_pseudo_trans. apply H4. apply plgs_sym. assumption. induction H7. induction H7. unfold TS in H7. spliter. unfold Parallelogram_flat in *. spliter. apply False_ind. apply H10. assert(Col C D A). ColR. assert(Col C D B). ColR. apply (col3 C D); Col. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates