proposition: Lemma perp_acute_out : forall A B C C', Acute A B C -> Perp A B C C' -> Col A B C' -> Out B A C'.
proof: Proof. intros. apply l6_6. apply acute_col_perp__out with C. apply acute_sym. assumption. Col. Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles