proposition: Lemma plg_plg_bet : forall A B C D B' C', Parallelogram A B C D -> Bet A B B' -> Parallelogram A B' C' D -> Bet D C C'.
proof: Proof. intros. induction(eq_dec_points A B). subst B. induction H. apply False_ind. apply H. apply plgs_sym in H. apply False_ind. apply H. Col. apply plgf_trivial_neq in H. spliter. subst D. Between. induction (eq_dec_points B C). subst C. induction H. apply False_ind. apply plgs_sym in H. apply H. Col. apply plgf_permut in H. apply plgf_trivial_neq in H. spliter. subst D. induction H1. apply False_ind. apply H. Col. apply plgf_permut in H. apply plgf_sym in H. apply plgf_trivial_neq in H. spliter. subst C'. Between. assert(A <> B'). intro. subst B'. apply between_identity in H0. contradiction. assert(B' <> C'). intro. subst C'. apply plg_permut in H1. induction H1. apply plgs_par_strict in H1. spliter. apply H1. exists A. split; Col. apply plgf_trivial_neq in H1. spliter. subst D. apply plg_permut in H. induction H. apply plgs_par_strict in H. spliter. apply H1. exists A. split; Col. apply plgf_sym in H. apply plgf_trivial_neq in H. tauto. assert(HH:=H). assert(HH1:=H1). apply plg_par in H; auto. apply plg_par in H1; auto. spliter. assert(Par A B C' D). apply (par_col_par_2 _ B'); auto. apply bet_col in H0. Col. assert(Col C' C D /\ Col D C D). apply(parallel_uniqueness A B C D C' D D); Col. spliter. clear H10. induction HH; induction HH1. apply (plgs_plgs_bet A B _ _ B'). apply H10. apply H0. auto. apply False_ind. unfold Parallelogram_flat in H11. spliter. apply plgs_par_strict in H10. spliter. apply bet_col in H0. apply H10. assert(Col A B C'). ColR. exists C'. split; Col. apply False_ind. unfold Parallelogram_flat in H10. spliter. apply plgs_par_strict in H11. spliter. apply bet_col in H0. apply H11. assert(Col A B' C). ColR. exists C. split; Col. apply (plgf_plgf_bet A B _ _ B'). apply H10. apply H0. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec