proposition: Lemma bet_le_le : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le A B A' B' -> Le B C B' C' -> Le A C A' C'.
proof: Proof. intros. assert(HH1:=H1). assert(HH2:=H2). unfold Le in HH1. unfold Le in HH2. ex_and HH1 X. ex_and HH2 Y. assert(Le A C A' Y). eapply le_cong_le with B B'. apply H. eapply between_inner_transitivity. apply H0. assumption. assumption. assumption. induction (eq_dec_points B' Y). subst Y. assert(Le A' B' A' C'). unfold Le. exists B'. split. assumption. apply cong_reflexivity. eapply le_transitivity. apply H7. assumption. assert(Bet A' Y C'). eapply outer_transitivity_between2 with B'. eapply between_inner_transitivity. apply H0. assumption. assumption. auto. eapply le_transitivity. apply H7. unfold Le. exists Y. split. assumption. apply cong_reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec