proposition: Lemma inner_pasch_B : forall A B C P Q, BetH A P C -> BetH B Q C -> ~ ColB A B C -> exists x, BetH P x B /\ BetH Q x A.
proof: Proof. intros A B C P Q HBetH1 HBetH2 HNC. unfold BetH in HBetH1. destruct HBetH1 as [HBet1 [HAP HPC]]. unfold BetH in HBetH2. destruct HBetH2 as [HBet2 [HBQ HQC]]. apply NColB_NColOrEq in HNC. assert (HIP := inner_pasch A B C P Q HBet1 HBet2). destruct HIP as [x [HBet3 HBet4]]. exists x. split. split; try assumption. split. intro. subst. apply HNC. assert_cols. ColR. intro. subst. apply HNC. assert_cols. ColR. split; try assumption. split. intro. subst. apply HNC. assert_cols. ColR. intro. subst. apply HNC. assert_cols. ColR. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality