proposition: Lemma perp_out__acute : forall A B C C', Perp A B C C' -> Col A B C' -> (Acute A B C <-> Out B A C').
proof: Proof. intros. split. intro. apply (perp_acute_out _ _ C); auto. intro. apply (perp_out_acute _ _ C C'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms