proposition: Lemma angle_partition : forall A B C, A <> B -> B <> C -> Acute A B C \/ Per A B C \/ Obtuse A B C.
proof: Proof. intros A B C HAB HBC. assert(Hl := lower_dim_ex). destruct Hl as [A' [B' [D']]]. assert(~ Col A' B' D') by (unfold Col; auto). assert(HC' := l10_15 A' B' B' D'). destruct HC' as [C' [HC'Right _]]; Col. assert_diffs. destruct (or_lta2_conga A B C A' B' C') as [|[|]]; auto. - left. exists A', B', C'. repeat (split; Perp). - right; right. exists A', B', C'. repeat (split; Perp). - right; left. apply (l11_17 A' B' C'); try (apply conga_sym); Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2