proposition: Lemma cong_lt_per2__lt_1 : forall A B C A' B' C', Per A B C -> Per A' B' C' -> Lt A B A' B' -> Cong A C A' C' -> Lt B' C' B C.
proof: Proof. intros. apply nle__lt. intro. destruct (le_lt_per2__lt C B A C' B' A'); Perp; Le; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2