proposition: Lemma th12: 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' -> CongaH B A C B' A' C' -> CongaH A B C A' B' C' /\ CongaH A C B A' C' B' /\ CongH B C B' C'.
proof: Proof. intros. repeat split. apply cong_5;auto. apply cong_5;auto. intro;apply H;Col. intro;apply H0;Col. apply conga_permlr;auto. assert (T:=ncolH_distincts A B C H). assert (U:=ncolH_distincts A' B' C' H0). spliter. elim (out_construction B' C' B C H8 H5). intros D' [HD1 HD2]. destruct (eq_dec_pointsH B' D'). { subst. unfold outH in HD2. destruct HD2. apply betH_expand in H10;intuition. destruct H10. apply betH_expand in H10;intuition. intuition. } assert (CongaH A B C A' B' C') by ( apply cong_5;auto). assert (CongaH B A C B' A' D'). apply (cong_5 B A C B' A' D'). intro;apply H;Col. intro;apply H0. apply outH_col in HD2. apply colH_trans with B' D';Col. apply congH_permlr;auto. apply congH_sym;auto. apply conga_out_conga with A C A' C'; auto using outH_trivial. assert (outH A' C' D'). apply (cong_4_uniqueness B A C A' C' B' C' D');try assumption. intro;apply H0;Col. intro;apply H;Col. apply same_side_prime_refl;auto. unfold same_side'. split. auto. intros. unfold same_side. destruct (between_out D' B'). auto. exists x. unfold cut. repeat split. intro. apply H0;exists l;auto. intro. apply outH_col in HD2. destruct HD2. spliter. apply betH_expand in H15. spliter. destruct H23. spliter. assert (EqL x1 l). apply line_uniqueness with B' x;auto. rewrite H26 in *. assert (EqL x0 l). apply line_uniqueness with B' D';auto. rewrite H27 in *. apply H0. exists l;auto. exists B'. split. auto. unfold outH in HD2. destruct HD2. apply (betH_trans0 D' C' B' x);auto using between_comm. destruct H16. apply between_comm;apply (betH_trans2 x B' D' C');auto using between_comm. spliter;subst;auto. intro. apply outH_col in HD2. assert (ColH A' B' D'). exists l;auto. apply H0. apply (colH_trans B' D' A' B' C');Col. intro. apply outH_col in HD2. destruct HD2. spliter. apply betH_expand in H15. spliter. destruct H23. spliter. assert (EqL x1 l). apply line_uniqueness with B' x;auto. rewrite H26 in *. assert (EqL x0 l). apply line_uniqueness with B' D';auto. rewrite H27 in *. apply H0. exists l;auto. exists B'. split. auto. auto. assert (C'=D'). line B' C' lB'C' H5. line A' C' lA'C' H6. apply inter_incid_uniquenessH with A' lB'C' lA'C';auto. intro. apply H0. exists lB'C';auto. apply outH_col in HD2. destruct HD2. spliter. assert (EqL x lB'C'). apply line_uniqueness with B' C';auto. rewrite H21 in H20. auto. apply outH_col in H13. destruct H13. spliter. assert (EqL x lA'C'). apply line_uniqueness with A' C';auto. rewrite H20 in H19. auto. subst. auto using congH_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