proposition: Lemma th17: forall X Y Z1 Z2 I, ~ ColH X Y Z1 -> ~ ColH X Y Z2 -> ColH X I Y -> BetH Z1 I Z2 -> CongH X Z1 X Z2 -> CongH Y Z1 Y Z2 -> CongaH X Y Z1 X Y Z2.
proof: Proof. intros. induction (colH_dec Y Z1 Z2). induction (colH_dec X Z1 Z2). { apply betH_expand in H2. spliter. exfalso. apply H0;ColHR. } { assert (CongaH X Z1 Z2 X Z2 Z1) by (apply (isosceles_congaH X Z1 Z2);auto). apply conga_permlr. apply (cong_5 Z1 Y X Z2 Y X). intro;apply H;Col. intro;apply H0;Col. apply congH_perms in H4;spliter; auto; try (intro; subst; Col). apply congH_perms in H3;spliter; auto; try (intro; subst; Col). apply conga_permlr. assert (BetH Z1 Y Z2). { apply ncolH_distincts in H; apply ncolH_distincts in H0; apply congH_colH_betH;apply betH_expand in H2;spliter;auto. } apply conga_out_conga with X Z2 X Z1;auto using outH_trivial. apply ncolH_distincts in H;spliter;auto using outH_trivial. unfold outH. right;left;auto. apply ncolH_distincts in H0;spliter;auto using outH_trivial. unfold outH. right;left;auto using between_comm. } induction (colH_dec X Z1 Z2). { assert (CongaH Y Z1 Z2 Y Z2 Z1) by (apply (isosceles_congaH Y Z1 Z2);auto). apply conga_permlr. apply (cong_5 Z1 Y X Z2 Y X). intro;apply H;Col. intro;apply H0;Col. apply congH_perms in H4;spliter; auto; try (intro; subst; Col). apply congH_perms in H3;spliter; auto; try (intro; subst; Col). assert (BetH Z1 X Z2) by (apply ncolH_distincts in H; apply ncolH_distincts in H0;apply congH_colH_betH;apply betH_expand in H2;spliter;auto). apply conga_out_conga with Y Z2 Y Z1;auto using outH_trivial. apply ncolH_distincts in H;spliter;auto using outH_trivial. unfold outH. right;left;auto. apply ncolH_distincts in H0;spliter;auto using outH_trivial. unfold outH. right;left;auto using between_comm. } assert (CongaH X Z1 Z2 X Z2 Z1) by (apply (isosceles_congaH X Z1 Z2);auto). assert (CongaH Y Z1 Z2 Y Z2 Z1) by (apply (isosceles_congaH Y Z1 Z2);auto). assert (CongaH X Z1 Y X Z2 Y). { apply th15 with Z2 Z1; auto; try solve[intro; apply H5; Col]; try solve[intro; apply H6; Col]; try solve[intro; apply H; Col]; try solve[intro; apply H0; Col]. destruct (plane_existence X Y Z1 H) as [p]; spliter. assert (IncidP Z2 p). { apply betH_colH in H2; spliter. apply (line_on_plane' Z1 I); trivial. apply ncolH_distincts in H; spliter. apply (line_on_plane' X Y); Col. } elim (plane_separation X Y Z1 Z2 p); Col; intro HS; [left|right]; split; auto; destruct HS; split; auto. } apply conga_permlr. apply (cong_5 Z1 Y X Z2 Y X);auto using conga_permlr, congH_perms. intro;apply H;Col. intro;apply H0;Col. apply congH_perms in H4;spliter; auto; try (intro; subst; Col). apply congH_perms in H3;spliter; auto; try (intro; subst; Col). 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