proposition: Lemma out_acute : forall A B C, Out B A C -> Acute A B C.
proof: Proof. intros. assert( A <> B /\ C <> B). unfold Out in H. tauto. spliter. assert(HH:= not_col_exists A B H0). ex_and HH Q. assert(exists P : Tpoint, Perp A B P B /\ OS A B Q P). apply(l10_15 A B B Q). Col. auto. ex_and H3 P. assert(Per P B A). apply perp_in_per. apply perp_left_comm in H3. apply perp_in_comm. apply perp_perp_in. Perp. unfold Acute. exists A. exists B. exists P. split. apply l8_2. auto. unfold LtA. split. unfold LeA. exists C. split. apply col_in_angle; auto. apply perp_not_eq_2 in H3. auto. apply conga_refl; auto. intro. apply l11_21_a in H6. apply perp_left_comm in H3. apply perp_not_col in H3. apply out_col in H6. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms