proposition: Lemma soustraction_betH : forall A B C A' B' C' : Point, BetH A B C -> BetH A' B' C' -> CongH A B A' B' -> CongH A C A' C' -> CongH B C B' C'.
proof: Proof. intros. apply betH_expand in H. apply betH_expand in H0. spliter. elim (segment_constructionH A' B' B C H3 H8). intros C1 [HC1 HC2]. assert (CongH A C A' C1). assert(HD := betH_distincts _ _ _ HC1); spliter. apply addition_betH with B B';auto using congH_sym. elim (between_out B A). intros X HX. elim (between_out B' A'). intros X' HX'. assert (BetH X A C). apply (betH_trans2 X A B C);auto using between_comm. assert (BetH X' A' C1). apply (betH_trans2 X' A' B' C1);auto using between_comm. assert (C'=C1). { apply construction_uniqueness with X' A'; auto. apply (betH_trans2 X' A' B' C'); auto using between_comm. apply cong_pseudo_transitivity with A C; auto using congH_sym. } subst. auto using congH_sym. auto. auto. Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms