proposition: Lemma perp_per_bet : forall A B C P, ~Col A B C -> Col A P C -> Per A B C -> Perp_at P P B A C -> Bet A P C.
proof: Proof. intros. assert( A <> C). intro. subst C. apply H. Col. assert(Bet A P C /\ A <> P /\ C <> P). apply(l11_47 A C B P); auto. Perp. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel