proposition: Lemma bet_double_bet : forall A B C B' C', Midpoint B' A B -> Midpoint C' A C -> Bet A B' C' -> Bet A B C.
proof: Proof. intros. unfold Midpoint in *. spliter. assert(Le A B' A C'). unfold Le. exists B'. split. assumption. apply cong_reflexivity. assert (Le B' B C' C). eapply l5_6. apply H4. assumption. assumption. assert(Le A B A C). eapply bet_le_le. apply H. apply H0. assumption. assumption. induction (eq_dec_points A B'). subst B'. apply cong_symmetry in H3. apply cong_identity in H3. subst B. apply between_trivial2. assert( A <> C'). intro. subst C'. apply le_zero in H4. contradiction. assert(A <> B). intro. subst B. apply between_identity in H. contradiction. assert(A <> C). intro. subst C. apply between_identity in H0. contradiction. assert(Out A B C). assert(Bet A B C' \/ Bet A C' B). eapply l5_1. apply H7. assumption. assumption. induction H11. eapply l6_7. apply bet_out. auto. apply H11. apply bet_out. auto. assumption. assert(Bet A B C \/ Bet A C B). apply l5_1 with C'. auto. assumption. assumption. induction H12. apply bet_out. auto. assumption. apply l6_6. apply bet_out. auto. assumption. eapply l6_13_1. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec