proposition: Lemma triangle_strict_reverse_inequality : forall A B C D, Out A B D -> Cong A C A D -> ~ Out A B C -> Lt B D B C.
proof: Proof. intros A B C D HABD HCong HNout. elim(col_dec A B C). { intro. assert_diffs. apply not_out_bet in HNout; Col. assert(Bet D A C) by (apply (l6_2 B); auto). assert(C <> D) by (intro; treat_equalities; auto). split. { destruct HABD as [_ [_ [HABD|HADB]]]. - apply (le_transitivity _ _ A D). apply le_comm; exists B; split; Between; Cong. apply (l5_6 C A C B); Cong. exists A; split; Between; Cong. - exists D. split; Cong. apply (outer_transitivity_between _ _ A); Between. } intro. absurd (A = B); auto. apply (l7_17 D C); split; Cong. apply l7_20_bis; auto; ColR. } intro HNCol. assert_diffs. elim(eq_dec_points B D). { intro. subst. split; Le. intro; treat_equalities; auto. } intro. assert(HNCol2 : ~ Col B C D) by (intro; apply HNCol; ColR). assert(HNCol3 : ~ Col A C D) by (intro; apply HNCol; ColR). assert_diffs. apply l11_44_2; Col. assert(CongA A C D A D C) by (apply l11_44_1; Cong; Col). destruct HABD as [_ [_ [HABD|HADB]]]. - apply between_symmetry in HABD. apply (conga_preserves_lta D C B D C A). apply conga_pseudo_refl; auto. apply (l11_10 D C A A D C); [apply conga_left_comm|try (apply out_trivial)..]; auto. apply bet_out; auto. split. { exists B. split; [|apply conga_refl; auto]. repeat split; auto. exists B. split; auto. right; apply out_trivial; auto. } intro. assert (Out C B A). { apply (conga_os__out D); trivial. apply out_one_side; [Col|Out]. } apply HNCol; Col. - assert(HE := symmetric_point_construction B C). destruct HE as [E []]. assert_diffs. apply (bet2_lta__lta A _ _ E); Between. assert (OS D C A E). { exists B. repeat split; Col. exists D; Col. intro; apply HNCol2; ColR. exists C; split; finish. } apply (conga_preserves_lta A C D E C D); try (apply conga_refl); auto. split. { apply lea_comm. exists A. split; [|apply conga_refl; auto]. apply os2__inangle; Side. apply (col_one_side _ B); Col. apply invert_one_side. apply out_one_side; Col. apply bet_out; Between. } intro. assert (Out C A E). apply (conga_os__out D); [apply conga_comm|]; assumption. apply HNCol; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2