proposition: Lemma plgf_plgf_bet : forall A B C D B' C', Parallelogram_flat A B C D -> Bet A B B' -> Parallelogram_flat A B' C' D -> Bet D C C'.
proof: Proof. intros. induction (eq_dec_points A B). subst B. assert(C = D /\ A <> C). apply plgf_trivial_neq. auto. spliter. subst D. Between. assert(HH:=not_col_exists A B H2). ex_and HH P. assert(HH:=plg_existence A B P H2). ex_and HH Q. assert(Parallelogram_strict A B P Q). induction H4. assumption. unfold Parallelogram_flat in H4. spliter. contradiction. assert(Parallelogram_strict C D Q P). apply(plgf_plgs_trans C D A B P Q). intro. subst D. assert(A = B /\ C <> A). apply plgf_trivial_neq. apply plgf_sym. assumption. tauto. apply plgf_sym. assumption. assumption. assert(A <> B'). intro. subst B'. apply between_identity in H0. contradiction. assert(HH:=vector_construction A B' Q). ex_and HH P'. induction H8; [|tauto]. assert(B <> P). intro. subst P. apply H3. Col. assert(B' <> P'). intro. subst P'. induction H8. apply plgs_par_strict in H8. spliter. apply H10. apply plgs_par_strict in H5. exists A. split; Col. apply plgf_permut in H8. assert(Q = A /\ B' <> Q). apply plgf_trivial_neq. auto. spliter. subst Q. apply H5. Col. assert(Par A B' P Q). apply plg_par in H8; auto. spliter. apply bet_col in H0. apply (par_col_par_2 _ B); auto. apply plg_par in H4; auto. spliter. assumption. assert(Col P' P Q /\ Col Q P Q). apply(parallel_uniqueness A B' P Q P' Q Q ); Col. apply plg_par in H8; auto. spliter. auto. spliter. clear H13. assert(Parallelogram_strict A B' P' Q). induction H8. auto. unfold Parallelogram_flat in H8. spliter. apply False_ind. unfold Parallelogram_flat in *. spliter. apply bet_col in H0. assert(Col B' P' Q). ColR. apply plgs_par_strict in H5. spliter. apply H5. exists Q. split. ColR. Col. assert(Parallelogram_strict D C' P' Q). apply (plgf_plgs_trans _ _ B' A). intro. subst C'. apply plgf_sym in H1. apply plgf_trivial_neq in H1. tauto. apply plgf_comm2. apply plgf_sym. apply H1. apply plgs_comm2. assumption. assert(Bet Q P P'). apply(plgs_plgs_bet A B P Q B' P'); auto. apply(plgs_plgs_bet Q P C D P' C'). apply plgs_sym. auto. auto. apply plgs_comm2. apply plgs_sym. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec