proposition: Lemma acute_col_perp__out : forall A B C A', Acute A B C -> Col B C A' -> Perp B C A A' -> Out B A' C.
proof: Proof. intros A B C A' HacuteB HBCA' HPerp. assert(HUn := perp_not_col2 B C A A' HPerp). destruct HUn as [HNCol1|]; [|contradiction]. assert(HB' := l10_15 B C B A). destruct HB' as [B' []]; Col. assert_diffs. assert(HNCol2 : ~ Col B' B C ) by (apply per_not_col; Perp). assert(HNCol3 : ~ Col B B' A). { intro. apply (nlta A B C). apply acute_per__lta; auto. apply (l8_3 B'); Col; Perp. } assert(HPars : Par_strict B B' A A'). apply (par_not_col_strict _ _ _ _ A); Col; apply (l12_9 _ _ _ _ B C); Perp; Cop. assert(HNCol4 := par_strict_not_col_4 B B' A A' HPars). apply (col_one_side_out _ B'); Col. apply (one_side_transitivity _ _ _ A). apply l12_6; Par. apply invert_one_side. apply in_angle_one_side; Col. apply l11_24. apply lea_in_angle; Side. apply lta_comm. apply acute_per__lta; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles