proposition: Lemma out__acute : forall A B C, Out B A C -> Acute A B C.
proof: Proof. intros A B C Hout. assert_diffs. assert(HD := perp_exists B A B). destruct HD as [D]; auto. assert_diffs. exists A. exists B. exists D. split; Perp. split. apply l11_31_1; auto. intro. assert(HNCol : ~ Col A B D) by (apply per_not_col; Perp). apply HNCol. apply col_permutation_4. apply out_col. apply (l11_21_a A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2