proposition: Lemma segment_addition (a b c a' b' c' : Vector): cong a b a' b' -> cong b c b' c' -> bet a b c -> bet a' b' c' -> cong a c a' c'.
proof: Proof. case: (a =P b). move ->. rewrite cong_cdab=> H. by rewrite (POF_to_Tarski.cong_identity H). move=> /eqP ab_neq cong_aba'b' cong_bcb'c' bet_abc bet_a'b'c'. rewrite cong_bacd cong_abdc. apply POF_to_Tarski.five_segment with a a' b b'=> //. by rewrite cong_aaxx. by rewrite cong_bacd cong_abdc. by apply /eqP. 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