proposition: Lemma lam_lt__obtuse : forall A B C D, Lambert A B C D -> Lt B C A D -> Obtuse B C D.
proof: Proof. intros A B C D HLam HLt. assert (HLam' := HLam). unfold Lambert in HLam'. spliter. exists A, D, C. split; trivial. apply lta_left_comm, lt_os_per2__lta; Perp; [|apply lt_right_comm; trivial]. apply invert_one_side, l12_6, lam__pars1234, HLam. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma