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