proposition: Lemma cong_lt_per2__lt : forall A B C A' B' C', Per A B C -> Per A' B' C' -> Cong A B A' B' -> Lt B C B' C' -> Lt A C A' C'.
proof: Proof. intros. destruct (eq_dec_points A B). treat_equalities; auto. destruct (eq_dec_points B C). subst C. apply (cong2_lt__lt B' A' C' A'); Cong. assert_diffs. apply l11_46; Perp. destruct H2 as [[C0 []] HNCong]. assert_diffs. assert (Per A' B' C0) by (apply per_col with C'; Col). apply (cong2_lt__lt A' C0 A' C'); [|apply l10_12 with B' B|]; Cong. apply lt_comm. destruct (l11_53 C' C0 B' A'); Between. intro; subst; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2