proposition: Lemma obtuse_sym : forall A B C, Obtuse A B C -> Obtuse C B A.
proof: Proof. unfold Obtuse. intros. ex_and H A'. ex_and H0 B'. ex_and H C'. exists A'. exists B'. exists C'. split. assumption. apply lta_right_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2