proposition: Lemma bet_intersect (a b c d e x y : (@Vector R 1)) : ~(bet c e d \/ bet e d c \/ bet d c e) -> a != b -> c != d -> bet a e c -> bet a b x -> bet c d x -> bet a b y -> bet c d y -> x = y.
proof: Proof. move=> ncol /eqP ab_neq /eqP cd_neq bet_aec bet_abx bet_cdx bet_aby bet_cdy. apply l6_21 with a b c d; try apply Ch03_bet.bet_col ; auto. move=> col ; apply ncol. apply col_transitivity_1 with x; Col. move=> cx_eq; treat_equalities. have: c=d by exact (between_identity _ _ bet_cdx). by []. apply col_transitivity_1 with a; Col. move=> ca_eq; treat_equalities. have: c=e by exact (between_identity _ _ bet_aec). by move=> ce_eq; treat_equalities; apply ncol; left; rewrite bet_xxa. apply col_permutation_4; apply col_transitivity_1 with b; Col. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence