proposition: Lemma acute_sym : forall A B C, Acute A B C -> Acute C B A.
proof: Proof. unfold Acute. intros. ex_and H A'. ex_and H0 B'. ex_and H C'. exists A'. exists B'. exists C'. split;auto using lta_left_comm. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2