proposition: Lemma segment_addition' (a b c a' b' c' : Point): 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. rewrite -!dist_cong'. move=> /eqP cong'_aba'b' /eqP cong'_bcb'c' bet'_abc bet'_a'b'c'. apply bet_dist_bet' in bet'_abc. apply bet_dist_bet' in bet'_a'b'c'. move: bet'_abc bet'_a'b'c'. rewrite /bet_dist /bet_dist_v -!/(dist _ _) => /eqP -> /eqP ->. by rewrite cong'_aba'b' cong'_bcb'c' eqxx. 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