proposition: Lemma obtuse_per__lta : forall A B C D E F, Obtuse A B C -> D <> E -> E <> F -> Per D E F -> LtA D E F A B C.
proof: Proof. intros A B C D E F Hobtuse HDE HEF HPer. intros. destruct Hobtuse as [G [H [I [HPer2 Hlta]]]]. assert(Hdiff := lta_distincts G H I A B C Hlta). spliter. apply (conga_preserves_lta G H I A B C); try (apply conga_refl); auto. apply l11_16; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2