proposition: Lemma plgs_two_sides : forall A B C D, Parallelogram_strict A B C D -> TS A C B D /\ TS B D A C.
proof: Proof. intros. assert(HH:= plgs_mid A B C D H). ex_and HH M. unfold Parallelogram_strict in H. spliter. split. assumption. unfold TS. assert(~Col B A C). unfold TS in H. spliter. Col. assert(B <> D). intro. assert(HH:=one_side_reflexivity A C B H4). apply l9_9 in H. subst D. contradiction. unfold TS in H. assert(~ Col B A C). spliter. assumption. spliter. repeat split. intro. assert(Col M A B). unfold Midpoint in H1. spliter. apply bet_col in H1. ColR. apply H4. apply col_permutation_2. eapply (col_transitivity_1 _ M). intro. subst M. apply is_midpoint_id in H0. subst C. Col. unfold Midpoint in H0. spliter. apply bet_col. assumption. Col. intro. assert(Col M B C). unfold Midpoint in H1. spliter. apply bet_col in H1. ColR. apply H6. apply col_permutation_1. eapply (col_transitivity_1 _ M). intro. subst M. apply l7_2 in H0. apply is_midpoint_id in H0. subst C. Col. Col. unfold Midpoint in H0. spliter. apply bet_col in H0. Col. exists M. unfold Midpoint in *. spliter. apply bet_col in H1. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates