proposition: Lemma th14: forall A B C D A' B' C' D', ~ ColH A B C -> ~ ColH A' B' C' -> CongaH A B C A' B' C' -> BetH A B D -> BetH A' B' D' -> CongaH C B D C' B' D'.
proof: Proof. intros. apply betH_expand in H2. apply betH_expand in H3. spliter. assert (T:=ncolH_distincts A B C H). assert (U:=ncolH_distincts A' B' C' H0). spliter. elim (out_construction B' A' A B);try solve [auto]. intros A'' [HA1 HA2]. elim (out_construction B' C' B C);try solve [auto]. intros C'' [HC1 HC2]. elim (out_construction B' D' B D);try solve [auto]. intros D'' [HD1 HD2]. assert (CongaH B A C B' A'' C'' /\ CongaH B C A B' C'' A'' /\ CongH A C A'' C''). { apply (th12 B A C B' A'' C''). intro;apply H;Col. intro;apply H0. { destruct HA2. apply betH_expand in H19. spliter. destruct HC2. apply betH_expand in H24. spliter. apply colH_trans with B' A'';Col. apply colH_trans with B' C'';Col. destruct H24. apply betH_expand in H24. spliter. apply colH_trans with B' A'';Col. apply colH_trans with B' C'';Col. spliter;subst. exfalso. apply H0. apply colH_trans with B' A'';Col. destruct H19. apply betH_expand in H19. spliter. destruct HC2. apply betH_expand in H24. spliter. apply colH_trans with B' A'';Col. apply colH_trans with B' C'';Col. destruct H24. apply betH_expand in H24. spliter. apply colH_trans with B' A'';Col. apply colH_trans with B' C'';Col. spliter;subst. exfalso. apply H0. apply colH_trans with B' A'';Col. spliter;subst. exfalso. apply H0. destruct HC2. apply betH_expand in H20;spliter. apply colH_trans with B' C'';Col. destruct H20. apply betH_expand in H20;spliter. apply colH_trans with B' C'';Col. spliter;subst. apply colH_trans with A'' B';Col. } apply outH_expand in HA2; spliter. apply congH_sym; auto. apply cong_pseudo_transitivity with A B. auto using congH_sym. apply congH_perm; auto. apply outH_expand in HC2; spliter. auto using congH_sym. apply conga_out_conga with A C A' C'; auto using outH_trivial. } spliter. assert (BetH A'' B' D'') by (apply betH_outH2__betH with A' D';auto). apply betH_expand in H21. spliter. assert (CongH A D A'' D''). { apply addition_betH with B B';auto. apply congH_perms in HA1;intuition. apply congH_perms in HD1;intuition. } assert (~ ColH A C D). intro; apply H; apply colH_trans with A D;Col. assert (~ ColH A'' C'' D''). intro; apply H0. apply outH_expand in HA2. apply outH_expand in HC2. apply outH_expand in HD2. spliter;ColHR. assert (T:=ncolH_distincts A C D H27). assert (U:=ncolH_distincts A'' C'' D'' H28). spliter. assert (CongaH A C D A'' C'' D'' /\ CongaH A D C A'' D'' C'' /\ CongH C D C'' D''). { apply (th12 A C D A'' C'' D'');try assumption. apply conga_out_conga with C B C'' B'; auto using conga_permlr, outH_trivial. unfold outH;left;auto. left. apply betH_outH2__betH with A' D';auto. } spliter. assert (~ ColH D B C) by (intro; apply H; ColHR). assert (~ ColH D'' B' C''). apply outH_expand in HA2. apply outH_expand in HC2. apply outH_expand in HD2. intro;apply H0;spliter;ColHR. assert (T:=ncolH_distincts D B C H38). assert (U:=ncolH_distincts D'' B' C'' H39). spliter. assert (CongaH D B C D'' B' C''). { apply (cong_5 D B C D'' B' C''). assumption. assumption. apply congH_perms in HD1;spliter;auto. apply congH_perms in H37;spliter;auto. apply conga_out_conga with A C A'' C'';auto using outH_trivial. unfold outH. right;left;auto using between_comm. right;left. apply betH_outH2__betH with D' A';auto using between_comm. } apply conga_permlr. apply conga_out_conga with D C D'' C'';auto using outH_trivial, outH_sym. 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