proposition: Lemma th18_aux: forall A B C A' B' C', ~ ColH A B C -> ~ ColH A' B' C' -> CongH A B A' B' -> CongH A C A' C' -> CongH B C B' C' -> CongaH B A C B' A' C'.
proof: Proof. intros. assert (T:=ncolH_distincts A B C H). assert (U:=ncolH_distincts A' B' C' H0). spliter. elim (congaH_existence_congH C A B A' C' B' A B);try solve [intuition Col]. intros B0 [HA [HB HC]]. elim (between_out B' C');auto. intros P HP. elim (congaH_existence_congH C A B A' C' P A B);try solve [intuition Col]. intros B'' [HA'' [HB'' HC'']]. assert (~ ColH A' C' B0). intro. apply (same_side_prime_not_colH B' B0 A' C');intuition Col. assert (~ ColH A' C' B''). intro. apply (same_side_prime_not_colH P B'' A' C');intuition Col. assert (CongH B C B0 C'). { apply (th12 A B C A' B0 C'). intuition Col. intuition Col. apply ncolH_expand in H10; spliter. auto using congH_sym. auto. apply conga_permlr;auto. } assert (CongH B C B'' C'). { apply (th12 A B C A' B'' C'). intuition Col. intuition Col. apply ncolH_expand in H11; spliter. auto using congH_sym. auto. apply conga_permlr;auto. } assert (HA'B'' : A' <> B'') by (apply ncolH_expand in H11; spliter; auto). assert (HA'B0 : A' <> B0) by (apply ncolH_expand in H10; spliter; auto). assert (CongH A' B'' A' B0) by (apply cong_pseudo_transitivity with A B;auto using congH_sym). assert (CongH B'' C' B0 C') by (apply cong_pseudo_transitivity with B C;auto using congH_sym). assert (CongH A' B'' A' B') by (apply cong_pseudo_transitivity with A B;auto using congH_sym). assert (CongH B'' C' B' C') by (apply cong_pseudo_transitivity with B C;auto using congH_sym). elim (line_existence A' C' H6);intros l [HL1 HL2]. assert (cut l B' P). { unfold cut. split. intro;apply H0;exists l;auto. split. intro; apply H0. assert (ColH A' C' P) by (exists l;auto). apply betH_expand in HP;spliter;ColHR. exists C';split;assumption. } assert (cut l B' B''). { apply (cut_same_side_cut B' P B'' l);auto. unfold same_side' in *;spliter. specialize H20 with l. auto. } assert (exists I', ColH A' I' C' /\ BetH B' I' B''). { unfold cut in H19;spliter. elim H21;intros I' [HI1 HI2]. exists I';split. exists l;auto. auto. } destruct H20 as [I' [HI1' HI2']]. assert (exists I, ColH A' I C' /\ BetH B0 I B''). { assert (cut l B'' B0). { apply (cut_same_side_cut B'' B' B0 l). auto using cut_comm. unfold same_side' in HB. spliter. specialize H21 with l. apply H21;auto. } unfold cut in H20. spliter. destruct H22 as [I [HI1 HI2]]. exists I;split. exists l;auto. auto using between_comm. } destruct H20 as [I [HI1 HI2]]. assert (CongaH C' A' B'' C' A' B0). { apply (th17 C' A' B'' B0 I);intuition (Col || auto using between_comm). apply congH_perms in H15;spliter;auto; intro; subst; Col. } assert (CongaH C' A' B'' C' A' B'). { apply (th17 C' A' B'' B' I');intuition (Col || auto using between_comm). apply congH_perms in H17;spliter;auto;intro;subst;Col. } assert (outH A' B0 B'). { apply (cong_4_uniqueness C' A' B'' A' B' C' B0 B');try solve [intuition Col]. apply same_side_prime_refl;intuition Col. } apply conga_permlr; apply conga_out_conga with C B C' B0;auto using outH_trivial. intro;apply betH_expand in HP;spliter;apply H0;ColHR. 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