proposition: Lemma perp_obtuse_bet : forall A B C C', Perp A B C C' -> Col A B C' -> Obtuse A B C -> Bet A B C'.
proof: Proof. intros. assert(HH:= H1). unfold Obtuse in HH. ex_and HH A0. ex_and H2 B0. ex_and H3 C0. assert(A0 <> B0 /\ C0 <> B0 /\ A <> B /\ C <> B). unfold LtA in H3. spliter. unfold LeA in H3. ex_and H3 P. unfold CongA in H5. spliter. repeat split; auto. intro. subst C. apply perp_comm in H. apply perp_not_col in H. apply H. Col. spliter. assert(B <> C'). intro. subst C'. assert(Per A B C). apply perp_in_per. apply perp_in_comm. apply perp_perp_in. Perp. assert(CongA A0 B0 C0 A B C). apply l11_16; auto. unfold LtA in H3. spliter. unfold LeA in H3. contradiction. induction H0. auto. assert(Out B A C'). unfold Out. repeat split; auto. induction H0. right. auto. left. Between. eapply (perp_out_acute _ _ C) in H9. apply obtuse_not_acute in H1. contradiction. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms