proposition: Lemma l11_47 : forall A B C H , Per A C B -> Perp_at H C H A B -> Bet A H B /\ A <> H /\ B <> H.
proof: Proof. intros. assert(HH1:= H1). unfold Perp_at in H1. spliter. assert(Per C H A). apply H5. apply col_trivial_1. apply col_trivial_1. assert(Perp C H A B). eapply l8_14_2_1a. apply HH1. induction (col_dec A C B). assert(A <> H). intro. subst H. apply H1. apply sym_equal. eapply per_col_eq. apply H0. assumption. intro. subst B. assert(Perp_at C C A A C). apply perp_perp_in. assumption. apply H2. eapply l8_14_3. apply HH1. assumption. apply False_ind. apply H9. eapply per_col_eq. apply l8_2. apply H6. apply (col_transitivity_1 _ B); Col. auto. apply not_col_distincts in H8. spliter. assert(A <> H). intro. subst A. assert(Per C H B). apply perp_in_per. assumption. apply H1. eapply l8_7. apply l8_2. apply H0. apply l8_2. assumption. assert(Per C H B). apply per_col with A; auto. assert(H <> B). intro. subst B. apply H10. eapply l8_7. apply H0. apply l8_2. assumption. assert(Lt H A A C /\ Lt H C A C). apply l11_46; auto. left. apply l8_2. assumption. assert(Lt C A A B /\ Lt C B A B). apply l11_46; auto. assert(Lt H B B C /\ Lt H C B C). apply l11_46; auto. left. Perp. split. unfold Lt in *. spliter. apply l5_12_b. Col. eapply le_transitivity. apply le_left_comm. apply H15. apply le_left_comm. assumption. eapply le_transitivity. apply H17. apply le_left_comm. assumption. split;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2