proposition: Lemma triangle_strict_inequality : forall A B C D, Bet A B D -> Cong B C B D -> ~ Bet A B C -> Lt A C A D.
proof: Proof. intros A B C D HBet HCong HNBet. elim(col_dec A B C). { intro. assert_diffs. apply not_bet_out in HNBet; Col. destruct HNBet as [_ [_ [HBAC|HBCA]]]. - split. { apply (le_transitivity _ _ B C). apply le_comm; exists A; split; Between; Cong. apply (l5_6 D B D A); Cong; exists B; split; Between; Cong. } intro. assert(A = B); auto. apply between_symmetry in HBAC. apply (l7_17 C D); split; Cong. apply (outer_transitivity_between _ _ B); auto. apply (outer_transitivity_between2 _ A); auto. - assert(Bet A C D) by (apply (between_exchange4 _ _ B); Between). split. exists C; split; Cong. intro. assert(C = D) by (apply (between_cong A); auto). subst D. assert(B = C); auto. apply (between_equality _ _ A); Between. } intro HNCol. assert_diffs. assert(A <> D) by (intro; treat_equalities; auto). assert(~ Col A C D) by (intro; apply HNCol; ColR). assert_diffs. apply between_symmetry in HBet. apply l11_44_2; Col. assert(CongA C D A D C B). { apply (l11_10 C D B D C B); try (apply out_trivial); auto; [|apply l6_6, bet_out; auto]. apply conga_comm. apply l11_44_1; Cong. intro; apply HNCol; ColR. } split. - apply lea_comm. exists B. repeat (split; auto). exists B. split; auto. right; apply out_trivial; auto. - intro. assert (Out C A B). { apply (conga_os__out D). apply (conga_trans _ _ _ C D A); auto; apply conga_sym, conga_comm; auto. apply out_one_side; [Col|Out]. } apply HNCol; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2