proposition: Lemma os3__lta : forall A B C D, OS A B C D -> OS B C A D -> OS A C B D -> LtA B A C B D C.
proof: Proof. intros A B C D HosC HosA HosB. assert(HE : InAngle D A B C) by (apply os2__inangle; Side). destruct HE as [_ [_ [_ [E [HEBet HUn]]]]]. assert(HNCol : ~ Col A B C) by (apply (one_side_not_col123 _ _ _ D); auto). assert_ncols. destruct HUn as [|HBout]. exfalso; subst; Col. assert(A <> E) by (intro; subst; Col5). assert(C <> E) by (intro; subst; Col5). assert_diffs. apply (lta_trans _ _ _ B E C). - destruct (l11_41 E A B C); auto. intro; apply HNCol; ColR. apply (conga_preserves_lta E A B B E C); try (apply conga_refl); auto. apply conga_left_comm, out2__conga. apply out_trivial; auto. apply l6_6, bet_out; auto. - assert(Out E D B). apply (col_one_side_out _ A); Col; apply invert_one_side; apply (col_one_side _ C); Col; Side. assert_diffs. destruct (l11_41 D E C B); auto. intro; apply HNCol; ColR. apply out2__bet; auto. apply (conga_preserves_lta D E C C D B); try (apply conga_pseudo_refl); auto. apply out2__conga. apply l6_6; assumption. apply out_trivial; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2