proposition: Lemma bet_le__lt : forall A B C D, Bet A D B -> A <> D -> D <> B -> Le A C B C -> Lt D C B C.
proof: Proof. intros A B C D HBet HAD HBD Hle. assert(HAB : B <> A) by (intro; treat_equalities; auto). apply lt_comm. elim(col_dec A B C). { intro. elim(bet_dec C D B). { intro. split. exists D; Cong. intro. apply HBD. apply (between_cong C); auto. } intro HNBet. apply not_bet_out in HNBet; try ColR. assert_diffs. assert(Bet C D A) by (apply (l6_2 B); try (apply l6_6); Between). assert(A <> C) by (intro; treat_equalities; auto). assert(Hout : Out A C B) by (apply (l6_7 _ _ D); [apply l6_6|]; apply bet_out; Between). assert(~ Bet A B C). { intro. apply HAB. apply (between_cong C); Between. apply le_anti_symmetry; Le. } assert(B <> C) by (intro; subst; Between). assert (Bet B C A). apply out2__bet; [apply not_bet_out; Col; Between|apply l6_6; assumption]. assert(HC' := symmetric_point_construction A C). destruct HC' as [C']. assert_diffs. assert(Bet C C' B). { apply l6_13_1. apply (l6_2 _ _ A); Between. apply (l5_6 A C B C); Cong. } apply (le3456_lt__lt _ _ C A); [|exists C'; split; Cong]. split. exists D; Cong. intro. apply HAD. symmetry. apply (between_cong C); Between. } intro HNCol. assert_diffs. apply l11_44_2. intro; apply HNCol; ColR. apply (lea123456_lta__lta _ _ _ C A B). - apply lea_out4__lea with C A C B; try apply out_trivial; auto; [|apply l6_6, bet_out; Between]. apply l11_44_2bis; Col; Le. - assert(~ Col D A C) by (intro; apply HNCol; ColR). assert_diffs. assert(HInter := l11_41 D A C B). destruct HInter; auto. apply (conga_preserves_lta D A C C D B); try (apply conga_refl); auto. apply (l11_10 D A C C A D); try (apply out_trivial); try (apply conga_pseudo_refl); auto. apply l6_6, bet_out; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2