proposition: Lemma bet2_le2__le2356 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le A B A' B' -> Le A' C' A C -> Le B' C' B C.
proof: Proof. intros A B C A' B' C' HBet HBet' HLe1 HLe2. elim(eq_dec_points A B). { intro; treat_equalities. apply (le_transitivity _ _ A' C'); auto. destruct (l5_12_a A' B' C'); auto. } intro. assert (A<>C) by (intro; treat_equalities; auto). destruct (l5_5_1 A B A' B' HLe1) as [B0 [HBet1 HCong1]]. assert (A<>B0) by (intro; treat_equalities; auto). destruct HLe2 as [C0 [HBet2 HCong2]]. assert (A<>C0) by (intro; treat_equalities; auto). assert (Bet A B0 C0). { apply l6_13_1. apply (l6_7 _ _ B); [|apply (l6_7 _ _ C)]; [apply l6_6| |apply l6_6]; apply bet_out; auto. apply (l5_6 A' B' A' C'); Cong. destruct (l5_12_a A' B' C'); auto. } apply (l5_6 B0 C0 B C); Cong; [apply (le_transitivity _ _ B C0)|]. destruct (l5_12_a B B0 C0); eBetween. destruct (l5_12_a B C0 C); eBetween. apply cong_commutativity; apply (l4_3 _ _ A _ _ A'); Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le