proposition: Lemma bet_outer_transitivity (a b c d: Vector): b!=c -> bet a b c -> bet b c d -> bet a c d.
proof: Proof. move=> bc_neq bet_abc bet_bcd. destruct (POF_to_Tarski.segment_construction a c c d) as [e [? ?]]. suffices: (e == d) => [/eqP <- //|]. apply one_side_cong_eq with b c=> //. rewrite bet_sym. by apply POF_to_Tarski.bet_inner_transitivity with a; rewrite bet_sym. 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