proposition: Lemma acute_col_perp__out_1 : forall A B C A', Acute A B C -> Col B C A' -> Perp B A A A' -> Out B A' C.
proof: Proof. intros A B C A' HAcute HCol HPerp. destruct (segment_construction A B A B) as [A0 [HA1 HA2]]. destruct (segment_construction C B C B) as [C0 [HC1 HC2]]. assert_diffs. assert (HNCol : ~ Col B A A') by (apply per_not_col; Perp). assert_diffs. apply l6_2 with C0; auto. apply not_out_bet. ColR. intro. apply (not_bet_and_out A B A0); split; trivial. apply acute_col_perp__out with A'; Col. apply acute_sym, (acute_conga__acute A B C); auto. apply l11_14; auto. apply between_symmetry, l6_2 with C0; Between. apply l6_6; assumption. apply perp_col with A; Col; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles