proposition: Lemma lta123234_os_per2__lt : forall A B C D, Per B A D -> Per A D C -> OS A D B C -> LtA A B C B C D -> Lt D C B A.
proof: Proof. intros. apply lta_os_per2__lt; Perp; Side. apply lta_comm; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma