proposition: Lemma plgf_bet : forall A B A' B', Parallelogram_flat A B B' A' -> Bet A' B' A /\ Bet B' A B \/ Bet A' A B' /\ Bet A B' B \/ Bet A A' B /\ Bet A' B B' \/ Bet A B A' /\ Bet B A' B'.
proof: Proof. intros. induction H. spliter. induction(eq_dec_points A B). subst B. apply cong_symmetry in H1. apply cong_identity in H1. subst B'. left. split; Between. assert(A' <> B'). intro. subst B'. apply cong_identity in H1. contradiction. assert(Col A' B' A). ColR. assert(Col A' B' B). ColR. induction H0. right; right; right. split. assumption. apply (col_cong2_bet1 A); Col; Cong. induction H0. right;right; left. split. Between. eapply(col_cong2_bet2 _ A). Col. Between. Cong. Cong. induction H. assert(Bet A' B B'). eapply (outer_transitivity_between2 _ A); auto. assert(B = B' /\ A' = A). apply(bet_cong_eq A' A B B' H0 H8). Cong. spliter. subst B'. subst A'. right;left. split; Between. induction H. right;left. split;auto. eapply (between_inner_transitivity _ _ _ B); Between. Between. induction(eq_dec_points A A'). subst A'. apply cong_symmetry in H2. apply cong_identity in H2. subst B'. right;left. split; Between. left. split. assert(Bet A B' A' \/ Bet A A' B'). eapply (l5_2 B). auto. Between. Between. induction H9. Between. assert(Bet B' A' B). eapply (outer_transitivity_between _ _ A). Between. assumption. auto. assert(Bet B A' B'). eapply (outer_transitivity_between2 _ A). Between. assumption. assumption. assert(A = B /\ B' = A'). apply(bet_cong_eq); Between; Cong. spliter. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel