proposition: Lemma t18_18_aux : forall A B C D E F, Cong A B D E -> Cong A C D F -> LtA F D E C A B -> ~ Col A B C -> ~ Col D E F -> Le D F D E -> Lt E F B C.
proof: Proof. intros A B C D E F HCongAB HCongAC Hlta HNCol1 HNCol2 Hle. assert (Hd := Hlta). apply lta_distincts in Hd. spliter. assert(HG0 := angle_construction_1 C A B F D E). destruct HG0 as [G0 []]; Col. assert(~ Col F D G0) by (apply (one_side_not_col123 _ _ _ E); auto). assert_diffs. assert(HG := segment_construction_3 D G0 A B). destruct HG as [G []]; auto. assert(CongA C A B F D G). apply (l11_10 C A B F D G0); try (apply out_trivial); auto; apply l6_6; auto. assert(OS F D G E). { apply (one_side_transitivity _ _ _ G0); auto. apply invert_one_side. apply out_one_side; Col. apply l6_6; auto. } assert(HNCol3 : ~ Col F D G) by (apply (one_side_not_col123 _ _ _ E); auto). clear dependent G0. assert_diffs. assert(HSAS := l11_49 C A B F D G). destruct HSAS as [HCongBC _]; Cong. apply (cong2_lt__lt F E F G); Cong. apply (conga_preserves_lta _ _ _ _ _ _ F D E F D G) in Hlta; try (apply conga_refl); auto. assert(Cong D G D E) by (apply (cong_transitivity _ _ A B); auto). clear dependent A. clear dependent B. assert(~ Col E F G). { intro. destruct Hlta as [Hlea HNConga]. apply HNConga. assert (HSSA := l11_52 E F D G F D). destruct HSSA as [_[]]; Cong; Le. apply (l11_10 G F D G F D); try (apply out_trivial); try (apply conga_refl); auto. apply l6_6, (col_one_side_out _ D); Col. } assert(~ Col D E G). { intro. destruct Hlta as [Hlea HNConga]. apply HNConga. apply (l11_10 F D G F D G); try (apply out_trivial); try (apply conga_refl); auto. apply (col_one_side_out _ F); Col; Side. } apply l11_44_2; Col. assert(HInAngle : InAngle E F D G) by (apply lea_in_angle; destruct Hlta; auto). rename H into HFD. destruct HInAngle as [_ [_ [_ [H [HH HUn]]]]]. destruct HUn. exfalso; subst; Col. assert(H <> F) by (intro; subst; apply HNCol2; Col). assert(H <> G) by (intro; subst; Col5). assert(Hlt : Lt D H D E). { apply (cong2_lt__lt H D G D); Cong. apply (bet_le__lt F); auto. apply (l5_6 D F D E); Cong. } destruct Hlt. assert(H <> E) by (intro; subst; Cong). assert(Bet D H E) by (apply l6_13_1; Le). assert_diffs. assert(OS E G F D). { apply (one_side_transitivity _ _ _ H); [apply invert_one_side; apply one_side_symmetry|]; apply out_one_side; Col; apply bet_out; Between. } apply (lta_trans _ _ _ D E G). - apply(conga_preserves_lta F G E D G E); try (apply conga_refl); auto. apply l11_44_1; Col. split. { apply lea_comm. exists F. split; try (apply conga_refl); auto. repeat split; auto. exists H. split; Between. right; apply bet_out; Between. } intro HConga. apply conga_comm in HConga. assert (Out G F D) by (apply (conga_os__out E); assumption). apply HNCol3; Col. - apply lta_comm. split. { exists D. split; [|apply conga_refl; auto]. repeat split; auto. exists H. split; Between. right; apply bet_out; Between. } intro HConga. assert (Out E D F) by (apply (conga_os__out G); Side). apply HNCol2; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2