proposition: Lemma l3_17 : forall A B C A' B' P, Bet A B C -> Bet A' B' C -> Bet A P A' -> exists Q, Bet P Q C /\ Bet B Q B'.
proof: Proof. intros. assert (exists Q', Bet B' Q' A /\ Bet P Q' C) by (eapply inner_pasch;eBetween). ex_and H2 x. assert (exists y, Bet x y C /\ Bet B y B') by (eapply inner_pasch;eBetween). ex_and H4 y. exists y;eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong