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