proposition: Lemma bet_cong3_bet : forall A B C A' B' C', A' <> B' -> B' <> C' -> A' <> C' -> BetH A B C -> ColH A' B' C' -> CongH A B A' B' -> CongH B C B' C' -> CongH A C A' C' -> BetH A' B' C'.
proof: Proof. intros. apply between_one in H3; auto. induction H3. assumption. induction H3. apply between_comm in H3. apply betH_expand in H2. spliter. assert(HH:=segment_constructionH B C B C H8 H8). ex_and HH B''. apply betH_expand in H3. apply betH_expand in H11. spliter. assert(BetH A B B'' /\ BetH A C B''). apply(betH_trans A B C B'' H2 H11 ). spliter. assert(CongH A B'' A' B'). { apply(addition A C B'' A' C' B'); auto. apply(colH_trans B C); Col. apply bet_disjoint; auto. apply bet_disjoint; auto. apply(cong_pseudo_transitivity C B); auto using congH_sym, congH_perml, cong_permr. } assert(CongH A B'' A B). { apply betH_distincts in H21; spliter. apply (cong_pseudo_transitivity A' B'); apply congH_sym; auto. } assert(~CongH A B A B''). { apply betH_not_congH; auto. } exfalso. apply H25. apply betH_distincts in H21; spliter. apply congH_sym; assumption. apply between_comm in H3. apply betH_expand in H2. apply betH_expand in H3. spliter. clean_duplicated_hyps. assert(exists E : Point, BetH C A E /\ CongH A E A B). { apply(segment_constructionH C A A B); auto. } ex_and H8 B''. apply betH_expand in H8. spliter. assert(CongH C B'' C' B'). { apply(addition C A B'' C' A' B'); auto. apply bet_disjoint; auto. apply bet_disjoint; auto. apply cong_permr, congH_perml; auto. apply (cong_pseudo_transitivity A B); auto using congH_sym. } assert(BetH B A B'' /\ BetH C B B''). { apply(betH_trans0 C B A B''); Bet. } spliter. assert(~CongH C B C B''). { apply betH_not_congH. assert(HH:=(betH_trans0 C B A B''));auto. } exfalso. apply H23. apply betH_distincts in H3; spliter. apply (cong_pseudo_transitivity C' B'); apply congH_sym; auto. apply cong_permr, congH_perml; 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