proposition: Lemma obtuse_distincts : forall A B C, Obtuse A B C -> A<>B /\ C<>B /\ A <> C.
proof: Proof. intros A B C Hobtuse. destruct Hobtuse as [x [y [z [HPer Hgta]]]]. apply gta_distincts in Hgta. spliter. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2