proposition: Lemma t18_19 : forall A B C D E F, A <> B -> A <> C -> Cong A B D E -> Cong A C D F -> Lt E F B C -> LtA F D E C A B.
proof: Proof. intros A B C D E F HAB HAC HCongAB HCongAC Hlt. assert_diffs. apply nlea__lta; auto. intro Hlea. elim(conga_dec C A B F D E). - intro. exfalso. destruct Hlt as [Hle HNCong]. apply HNCong. assert(HSAS := l11_49 C A B F D E). destruct HSAS; Cong. - intro. apply (not_and_lt E F B C). split; auto. apply (t18_18 D _ _ A); Cong. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2