proposition: Lemma bet2_le2__le1346 : 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 A B C A' B' C' HBet HBet' HleAB HleBC. elim(eq_dec_points A B). { intro. subst B. apply (le_transitivity _ _ B' C'); auto. apply le_comm. exists B'. split; Between; Cong. } intro. elim(eq_dec_points B C). { intro. subst C. apply (le_transitivity _ _ A' B'); auto. exists B'; Cong. } intro. assert(A' <> B') by (intro; subst B'; assert(A = B); auto; apply (le_zero _ _ A'); auto). assert(B' <> C') by (intro; subst C'; assert(B = C); auto; apply (le_zero _ _ B'); auto). destruct HleAB as [B0 []]. assert(A' <> B0) by (intro; subst B0; assert(A = B); auto; apply (cong_reverse_identity A'); Cong). assert(HC0 := segment_construction A' B0 B C). destruct HC0 as [C0 []]. assert(B0 <> C0) by (intro; subst C0; assert(B = C); auto; apply (cong_reverse_identity B0); auto). exists C0. split; [|apply (l2_11 _ B _ _ B0); Cong]. apply (outer_transitivity_between2 _ B0); auto. assert(Bet B0 B' C') by (apply between_symmetry; apply (between_inner_transitivity _ _ _ A'); Between). apply l6_13_1. - elim(eq_dec_points B0 B'). { intro. subst. apply (l6_2 _ _ A'); Between. } intro. apply (l6_7 _ _ B'). apply (l6_2 _ _ A'); Between. apply bet_out; auto. - apply (le_transitivity _ _ B' C'). apply (l5_6 B C B' C'); Cong. apply le_comm. exists B'. split; Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le