proposition: Lemma t18_18 : forall A B C D E F, Cong A B D E -> Cong A C D F -> LtA F D E C A B -> Lt E F B C.
proof: Proof. intros A B C D E F HCongAB HCongAC Hlta. assert (Hd := Hlta). apply lta_distincts in Hd. spliter. elim(col_dec A B C). { intro. elim(bet_dec B A C). - intro. assert(HC' := segment_construction E D A C). destruct HC' as [C' []]. apply (cong2_lt__lt E F E C'); Cong; [|apply (l2_11 _ D _ _ A); Cong]. apply (triangle_strict_inequality _ D); auto. apply (cong_transitivity _ _ A C); Cong. intro. destruct Hlta as [_ HNConga]. apply HNConga. apply conga_line; Between. - intro. exfalso. apply (nlta C A B). apply (lea123456_lta__lta _ _ _ F D E); auto. apply l11_31_1; auto. apply not_bet_out; Col; Between. } intro. elim(col_dec D E F). { intro. elim(bet_dec F D E). - intro. exfalso. apply (nlta F D E). apply (lea456789_lta__lta _ _ _ C A B); auto. apply l11_31_2; auto. - intro HNBet. apply not_bet_out in HNBet; Col. assert(HF' := segment_construction_3 A B A C). destruct HF' as [F' []]; auto. apply (cong2_lt__lt B F' B C); Cong. { apply (triangle_strict_reverse_inequality A); Cong. intro. destruct Hlta as [_ HNConga]. apply HNConga. apply l11_21_b; auto. apply l6_6; auto. } apply (out_cong_cong A _ _ D); auto. apply l6_6; auto. apply (cong_transitivity _ _ A C); auto. } intro. elim(le_cases D F D E); intro; [|apply lt_comm; apply lta_comm in Hlta]; apply (t18_18_aux A _ _ D); Cong; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2