proposition: Lemma lta_os_per2__lt : forall A B C D, Per B A D -> Per A D C -> OS A D B C -> LtA B C D A B C -> Lt A B C D.
proof: Proof. intros A B C D HPer1 HPer2 Hos HLtA. destruct (or_lt_cong_gt A B C D) as [Hlt | [Hlt | Hcong]]; trivial; exfalso. - unfold Gt in Hlt. apply lt_comm in Hlt. apply (not_and_lta B C D A B C). split; trivial. apply lt4321_os_per2__lta; trivial. - destruct HLtA as [HLeA HNCongA]. apply HNCongA. apply conga_sym, sac__conga. unfold Saccheri; repeat (split; trivial). Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma