proposition: Lemma impossible_case_1 : forall A B C x y, Bet A B x -> Bet C y A -> Par_strict B C x y -> False.
proof: Proof. intros A B C x y. intros HABx HACy HPar. apply between_symmetry in HABx. assert (HI := inner_pasch x C A B y HABx HACy); destruct HI as [I [HBCI HIxy]]. apply HPar; exists I; split; Col. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Annexes.perp_bisect GeoCoq.Tarski_dev.Ch12_parallel