proposition: Lemma lam_per__cong : forall A B C D, Lambert A B C D -> Per B C D -> Cong A D B C.
proof: Proof. intros A B C D HLam HPer. assert (HLam' := HLam). unfold Lambert in HLam'. spliter. destruct (or_lt_cong_gt A D B C) as [Habs|[HCong|Habs]]; trivial; exfalso; apply (nlta B C D). - apply acute_per__lta; trivial. apply (lam_lt__acute A); trivial. - apply obtuse_per__lta; trivial. apply (lam_lt__obtuse A); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma