proposition: Lemma axiom_five_segmentsH: forall A A' B B' C C' D D', A<>D -> A'<>D' -> B<>D -> B'<>D' -> C<>D -> C'<>D' -> CongH A B A' B' -> CongH B C B' C' -> CongH A D A' D' -> CongH B D B' D' -> BetH A B C -> BetH A' B' C' -> A' <> D' -> CongH C D C' D'.
proof: Proof. intros. induction (colH_dec A B D). - apply betH_expand in H9. apply betH_expand in H10. spliter. apply between_one in H12; try assumption. assert (CongH A C A' C') by (apply addition_betH with B B';assumption). decompose [or] H12;clear H12. { assert (BetH A' B' D') by (apply cong_preserves_bet with A B D;try assumption). assert (HB:BetH A' D' C' \/ BetH A' C' D') by (apply (out2_out1 A' B' D' C');auto). destruct HB. assert (BetH A D C). assert (BetH B D C \/ BetH B C D) by ( apply (out2_out A B D C);auto). destruct H24. apply ( betH_trans A B D C);auto. exfalso. apply betH_congH2__False with B C D B' C' D';try assumption. apply (betH_trans0 A' B' D' C');auto. apply congH_permlr; apply betH_expand in H24; spliter; auto. apply (soustraction_betH A D C A' D' C');assumption. assert (BetH A C D). assert (HB:BetH A D C \/ BetH A C D) by (apply (out2_out1 A B D C);auto). destruct HB. exfalso. apply betH_congH2__False with A D C A' D' C';try assumption. assumption. apply (soustraction_betH A C D A' C' D');assumption. } { assert (BetH B' D' A'). apply cong_preserves_bet with B D A;auto. apply congH_permlr;auto. apply congH_permlr;auto. assert (BetH C D A). assert (T:=betH_trans0 A D B C). apply between_comm in H23. assert (U:=T H23 H9). spliter. apply between_comm;auto. assert (BetH C' D' A'). assert (T:=betH_trans0 A' D' B' C'). apply between_comm in H12. assert (U:=T H12 H10). spliter. apply between_comm;auto. apply congH_permlr; apply betH_expand in H24; spliter; auto. apply (soustraction_betH A D C A' D' C'); auto using between_comm. } { assert (BetH B' A' D'). apply cong_preserves_bet with B A D;auto. apply congH_permlr;auto. apply congH_permlr;auto. apply congH_permlr;auto. assert (BetH C' B' D'). apply betH_trans2 with A'. apply between_comm;auto. assumption. apply addition_betH with B B'. apply (betH_trans2 C B A D);auto using between_comm. assumption. apply congH_permlr;auto. assumption. } - apply betH_expand in H9;apply betH_expand in H10; spliter. assert (~ ColH A' B' D') by (intro;apply H12;apply cong_preserves_col_stronger with A' B' D';auto using congH_sym). assert (CongaH B A D B' A' D') by (apply th18_aux;assumption). assert (CongH A C A' C') by (apply addition with B B'; auto using between_col, bet_disjoint). apply (th12 A C D A' C' D');try assumption. intro. assert (A<>C) by (apply between_diff with B;auto). apply H12. apply colH_trans with A C;Col. apply between_col in H9;Col. intro;apply H12. apply cong_preserves_col_stronger with A' B' D';auto using congH_sym. apply betH_expand in H10;spliter; ColHR. assert (T:=ncolH_distincts A B D H12). decompose [and] T;clear T. apply conga_out_conga with B D B' D'; unfold outH;intuition idtac. 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