proposition: Lemma t22_14_aux : forall A B C, ~ Col A B C -> Acute A B C -> Acute A C B -> exists A', Bet B A' C /\ Per B A' A /\ Per C A' A /\ CongA B A' A C A' A /\ CongA A B C A B A' /\ CongA B C A A' C A /\ TS A A' B C.
proof: Proof. intros A B C HNCol HacuteB HacuteC. destruct (l8_18_existence B C A) as [A' [HCol HPerp]]; Col. exists A'. assert(Out B A' C) by (apply (acute_col_perp__out A); auto). assert(Out C A' B) by (apply (acute_col_perp__out A); Col; Perp). assert(Bet B A' C) by (apply (out2__bet); [|apply l6_6]; auto). assert_diffs. assert(Per B A' A) by (apply perp_per_1, perp_left_comm, (perp_col _ C); Col). assert(Per C A' A) by (apply (l8_3 B); Col). do 4 (split; [CongA|]). split; [|split]; [apply out2__conga; Out..|]. assert(~ Col B A' A) by (apply per_not_col; auto). apply invert_two_sides, bet__ts; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma