proposition: Lemma lam_obtuse__lt : forall A B C D, Lambert A B C D -> Obtuse B C D -> Lt B C A D.
proof: Proof. intros A B C D HLam HObtuse. destruct (or_lt_cong_gt A D B C) as [Habs|[Habs|HLt]]; trivial; exfalso; apply (nlta B C D). - apply acute_obtuse__lta; trivial. apply (lam_lt__acute A); trivial. - assert (HL := HLam). ex_and HL Hd. apply obtuse_per__lta; trivial. apply (cong_lam__per A); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma