proposition: Lemma bet_half_bet : forall A B C B' C', Bet A B C -> Midpoint B' A B -> Midpoint C' A C -> Bet A B' C'.
proof: Proof. intros. assert(HH0:= H0). assert(HH1:= H1). unfold Midpoint in H0. unfold Midpoint in H1. spliter. induction(eq_dec_points A B). subst B. apply between_identity in H0. subst B'. apply between_trivial2. assert(A <> C). intro. subst C. apply between_identity in H1. subst C'. apply between_identity in H. contradiction. assert(A <> B'). intro. subst B'. apply cong_symmetry in H3. apply cong_identity in H3. contradiction. assert(A <> C'). intro. subst C'. apply cong_symmetry in H2. apply cong_identity in H2. contradiction. assert(Col A B' C'). apply bet_col in H0. apply bet_col in H1. apply bet_col in H. ColR. induction H8. assumption. induction H8. apply between_symmetry in H8. assert(Bet A C B). eapply bet_double_bet. apply HH1. apply HH0. assumption. assert(B = C). eapply between_equality. apply between_symmetry. apply H9. Between. subst C. assert(B' = C'). eapply l7_17. apply HH0. assumption. subst C'. apply between_trivial. assert(Bet A B' C). eapply between_exchange4. apply H0. assumption. assert(Out A B' C'). unfold Out. repeat split; auto. eapply l5_3. apply H9. assumption. eapply l6_4_1 in H10. spliter. apply between_symmetry in H8. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel