proposition: Lemma perp_bet_obtuse : forall A B C C', B <> C' -> Perp A B C C' -> Bet A B C' -> Obtuse A B C.
proof: Proof. intros. assert(HPO:=perp_out_acute). assert(HBO:=acute_bet__obtuse). assert(Col A B C'). apply bet_col in H1. Col. assert(Acute C' B C). apply (HPO _ _ _ C'). apply out_trivial; auto. apply perp_left_comm. apply(perp_col _ A); Perp. Col. apply (HBO C'). Between. intro. subst B. apply perp_distinct in H0. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel