proposition: Lemma l11_43_aux : forall A B C, A <> B -> A <> C -> (Per B A C \/ Obtuse B A C) -> Acute A B C.
proof: Proof. intros. induction (col_dec A B C). induction H1. exfalso. apply (per_not_col B A C); Col. apply out__acute, bet_out; auto. apply col_obtuse__bet; Col. assert_diffs. prolong B A B' B A. assert(~ Col B' A C). intro. apply H2. eapply (col_transitivity_1 _ B'). intro. subst B'. apply cong_symmetry in H4. apply cong_identity in H4. subst A. apply H2. apply col_trivial_1. apply col_permutation_1. apply bet_col. assumption. apply col_permutation_4. assumption. apply not_col_distincts in H6. spliter. assert(LtA A C B C A B'/\ LtA A B C C A B'). apply l11_41. assumption. assumption. auto. spliter. induction H1. unfold Acute. exists C. exists A. exists B. split. apply l8_2. assumption. spliter. unfold LtA. unfold LtA in H11. spliter. assert(Per B' A C). apply l8_2. eapply (per_col _ _ B). assumption. apply l8_2. assumption. apply col_permutation_4. apply bet_col. assumption. assert(CongA B A C B' A C). apply l11_16. assumption. auto. auto. assumption. assumption. auto. split. eapply l11_30. apply H11. apply conga_refl. assumption. auto. apply conga_comm. apply conga_sym. assumption. intro. apply H12. eapply conga_trans. apply H15. apply conga_comm. assumption. unfold Acute. unfold Obtuse in H1. ex_and H1 a. ex_and H12 b. ex_and H1 c. assert(HH1:= H12). unfold LtA in H12. spliter. unfold LeA in H12. ex_and H12 P. exists B. exists A. exists P. assert(Per B A P). eapply l11_17. apply H1. assumption. split. assumption. assert(Per P A B'). eapply per_col. apply H. apply l8_2. assumption. apply col_permutation_4. apply bet_col. assumption. assert(CongA B A P B' A P). eapply l11_16. assumption. auto. intro. subst P. unfold CongA in H14. spliter. absurde. apply l8_2. assumption. assumption. intro. subst P. unfold CongA in H14. spliter. absurde. assert(LtA C A B' P A B). assert(B <> A). auto. assert(HH := l11_36 B A P B A C B' B' H18 H7 H18 H7 H3 H3). destruct HH. unfold LtA. split. eapply l11_30. apply H19. unfold LtA in HH1. spliter. eapply l11_30. apply H21. assumption. apply conga_refl. auto. auto. apply conga_left_comm. apply conga_refl. auto. assumption. apply conga_right_comm. apply conga_sym. assumption. intro. apply H13. assert(Per B' A C). eapply l11_17. apply H15. apply conga_comm. apply conga_sym. assumption. assert(Per C A B). eapply (per_col _ _ B'). auto. apply l8_2. assumption. apply col_permutation_1. apply bet_col. assumption. apply l11_16. assumption. unfold CongA in H14. spliter. assumption. unfold CongA in H14. spliter. assumption. apply l8_2. assumption. auto. auto. eapply lta_trans. apply H11. apply lta_right_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2