proposition: Lemma plgs_plgs_bet : forall A B C D B' C', Parallelogram_strict A B C D -> Bet A B B' -> Parallelogram_strict A B' C' D -> Bet D C C'.
proof: Proof. intros. assert(Col C' C D /\ Col D C D). apply (parallel_uniqueness A B C D C' D D); Col. left. apply plgs_par_strict in H. spliter. assumption. apply (par_col_par_2 _ B'). intro. subst B. apply plgs_par_strict in H. spliter. apply H. exists C. split; Col. apply bet_col in H0. Col. apply plgs_par_strict in H1. spliter. left. assumption. spliter. clear H3. induction H2. Between. induction H2. apply False_ind. apply plgs_permut in H. apply plgs_permut in H1. assert(HH1:=plgs_one_side B C D A H). assert(HH2:=plgs_one_side B' C' D A H1). spliter. assert(OS D A C C'). apply (one_side_transitivity _ _ _ B). apply one_side_symmetry. apply H6. apply one_side_symmetry. apply (one_side_transitivity _ _ _ B'). apply one_side_symmetry. apply H4. apply (out_one_side_1 _ _ _ _ A). intro. apply plgs_par_strict in H1. spliter. apply H1. exists B'. split; Col. Col. repeat split. intro. subst B'. apply H1. Col. intro. subst B. apply H. Col. right. assumption. assert(TS D A C C'). repeat split. intro. apply plgs_par_strict in H. spliter. apply H. exists C. split; Col. intro. apply plgs_par_strict in H1. spliter. apply H1. exists C'. split; Col. exists D. split. Col. assumption. apply l9_9 in H8. contradiction. assert(Parallelogram_strict B C D A). apply plgs_permut. assumption. assert(Parallelogram_strict D A B' C'). apply plgs_permut. apply plgs_sym. assumption. induction (eq_dec_points C C'). subst C'. Between. assert(HH:= plgs_pseudo_trans B C D A B' C' H3 H4). assert(Parallelogram_strict B C C' B'). induction HH. assumption. unfold Parallelogram_flat in H6. spliter. apply False_ind. apply plgs_par_strict in H. apply plgs_par_strict in H1. spliter. apply H. exists B. split. Col. apply bet_col in H2. ColR. assert(HH1:=plgs_one_side B C C' B' H6). assert(HH2:=plgs_one_side B C D A H3). spliter. assert(TS B C A B'). unfold TS. repeat split. intro. apply plgs_par_strict in H. spliter. apply H. exists C. split; Col. intro. apply plgs_par_strict in H6. spliter. apply H6. exists B'. split; Col. exists B. split. Col. assumption. assert(OS B C C' D). apply (out_one_side_1 _ _ _ _ C). intro. apply plgs_par_strict in H6. spliter. apply H6. exists C'. split; Col. apply col_trivial_2. repeat split. auto. intro. subst D. apply plgs_par_strict in H3. spliter. apply H3. exists C. split; Col. left. Between. assert(OS B C A B'). apply (one_side_transitivity _ _ _ D). apply one_side_symmetry. apply H7. apply (one_side_transitivity _ _ _ C'). apply one_side_symmetry. apply H12. assumption. apply l9_9 in H11. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec