proposition: Lemma one_side_cong'_eq (a b c d : Point): bet' a b c -> bet' a b d -> cong' b c b d -> a != b -> c == d.
proof: Proof. move=> bet_abc bet_abd cong_bcbd ab_neq. apply /eqP ; apply cong_identity with c. apply five_segment with a a b b; rewrite ?cong'_abab 1?cong'_cdab //; last by apply /eqP. by apply segment_addition' with b b; rewrite ?cong'_abab. 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