proposition: Lemma th15: forall H K O L H' K' O' L', ~ ColH H O L -> ~ ColH H' O' L' -> ~ ColH K O L -> ~ ColH K' O' L' -> ~ ColH H O K -> ~ ColH H' O' K' -> (cut' H K O L /\ cut' H' K' O' L') \/ (same_side' H K O L /\ same_side' H' K' O' L') -> CongaH H O L H' O' L' -> CongaH K O L K' O' L' -> CongaH H O K H' O' K'.
proof: Proof. assert (th15_aux : forall H K O L H' K' O' L', ~ ColH H O L -> ~ ColH H' O' L' -> ~ ColH K O L -> ~ ColH K' O' L' -> ~ ColH H O K -> ~ ColH H' O' K' -> same_side' H K O L -> same_side' H' K' O' L' -> CongaH H O L H' O' L' -> CongaH K O L K' O' L' -> CongaH H O K H' O' K'). { assert (th15_aux : forall H K O L H' K' O' L', ~ ColH H O L -> ~ ColH H' O' L' -> ~ ColH K O L -> ~ ColH K' O' L' -> ~ ColH H O K -> ~ ColH H' O' K' -> same_side' H K O L -> same_side' H' K' O' L' -> cut' K L O H -> CongaH H O L H' O' L' -> CongaH K O L K' O' L' -> CongaH H O K H' O' K'). { intros H K O L H' K' O' L' HNC1 HNC2 HNC3 HNC4 HNC5 HNC6. intros HOS1 HOS2 HCut' HConga1 HConga2. destruct (out_construction O' K' O K) as [K'' [HCong1 Hout1]]; try (intro; subst; Col). destruct (out_construction O' L' O L) as [L'' [HCong2 Hout2]]; try (intro; subst; Col). apply (conga_out_conga _ _ _ _ _ _ K L K'' L'') in HConga2; auto; try apply outH_sym; try apply outH_trivial; auto; try (intro; subst; Col). assert (HD1 : O <> H) by (intro; subst; Col). line O H l HD1; assert (HCut : cut l K L) by (destruct HCut' as [_ HCut]; apply HCut; auto). destruct HCut as [HNI1 [HNI2 [I [HI HBet1]]]]. assert (HD2 : O <> I) by (intro; subst; apply HNC3; apply between_col; auto). assert (HI' : exists I', O' <> I' /\ I' <> L'' /\ outH O H I /\ outH O' H' I' /\ ColH O' I' H' /\ CongH O' I' O I /\ CongaH I O L I' O' L''). { assert (outH O I H). { assert (HE : ColH O I H) by (exists l; auto). elim (eq_dec_pointsH H I); intro HD3; [subst; apply outH_trivial; auto|]. apply between_one in HE; auto; elim HE; clear HE; intro HE; [left; auto|]. elim HE; clear HE; intro HFalse; [right; left; apply between_comm; auto|]. assert (HD4 : O <> L) by (intro; subst; Col). line O L m HD4; destruct HOS1 as [_ HOS1]. assert (HF : same_side H K m) by (apply HOS1; auto). exfalso; apply (same_side_not_cut _ _ _ HF). apply cut_same_side_cut with I. { split; [intro; apply HNC1; exists m; auto|]. split; [|exists O; split; try apply between_comm; auto]. intro; assert (ColH O L I) by (exists m; auto). apply between_col in HFalse; apply HNC1; ColHR. } { apply out_same_side with L; try (left; apply between_comm); auto. intro; assert (ColH O L I) by (exists m; auto). apply between_col in HFalse; apply HNC1; ColHR. } } destruct (out_construction O' H' O I) as [I' [HCong3 Hout4]]; try (intro; subst; Col). apply (conga_out_conga _ _ _ _ _ _ I L I' L'') in HConga1; auto; try apply outH_sym; try apply outH_trivial; auto; try (intro; subst; Col). assert (O' <> I') by (apply outH_expand in Hout4; spliter; auto). assert (I' <> L''). { intro; subst; apply same_side_prime_not_colH in HOS2; destruct HOS2 as [HNC _]; apply HNC. apply outH_expand in Hout2; apply outH_expand in Hout4; spliter; ColHR. } exists I'; split; auto; split; auto; split; [apply outH_sym; auto|]. split; auto; split; try apply outH_col; try apply outH_sym; auto. } assert (HCol1 : ColH O I H) by (exists l; auto); clear HConga1. destruct HI' as [I' [HD3 [HD4 [Hout3 [Hout4 [HCol2 [HCong3 HConga1]]]]]]]. assert (HT : CongaH O I L O' I' L'' /\ CongaH O L I O' L'' I' /\ CongH I L I' L''). { assert (O <> L) by (intro; subst; Col). assert (O' <> L'') by (apply outH_expand in Hout2; spliter; auto). apply outH_expand in Hout2; spliter. apply th12; auto using congH_sym; try intro; [apply HNC1|apply HNC2]; ColHR. } destruct HT as [_ [HConga3 HCong4]]. assert (HT : CongaH O K L O' K'' L'' /\ CongaH O L K O' L'' K'' /\ CongH K L K'' L''). { assert (O <> K) by (intro; subst; Col). assert (O <> L) by (intro; subst; Col). apply outH_expand in Hout1; apply outH_expand in Hout2; spliter. apply th12; auto using congH_sym; intro; [apply HNC3|apply HNC4]; Col; ColHR. } destruct HT as [HConga4 [HConga5 HCong5]]. assert (HBet2 : BetH K'' I' L''). { assert (Hout5 : outH L'' I' K''). { assert (O <> K) by (intro; subst; Col). assert (O <> L) by (intro; subst; Col). apply outH_expand in Hout1; apply outH_expand in Hout2; spliter. apply cong_4_uniqueness with O L K H' O'; auto; [intro; apply HNC2; ColHR|intro; apply HNC3; Col| | |]. { apply conga_out_conga with O I O' I'; try apply outH_trivial; auto. left; apply between_comm; auto. } { assert (HD5 : O' <> L'') by auto; line O' L'' m HD5. apply out_same_side' with O' m; auto; intro; apply HNC2. assert (ColH O' L'' H') by (exists m; auto); ColHR. } { split; auto; destruct HOS2 as [_ HOS2]; intro m; intros. assert (HCol3 : ColH O' L' L'') by auto. destruct HCol3 as [o [HI1 [HI2 HI3]]]; assert (HEq := HI1). apply (line_uniqueness _ L'' m _) in HEq; auto; rewrite HEq. apply same_side_trans with K'; try apply HOS2; auto. apply out_same_side with O'; auto; intro; apply HNC4; exists o; auto. } } apply between_comm; assert (K <> L) by (intro; subst; Col). apply outH_expand in Hout5; apply betH_expand in HBet1; spliter. apply betH_congH3_outH_betH with L I K; try apply between_comm; try apply cong_permr, congH_perml; auto. } assert (HT : CongaH K O I K'' O' I' /\ CongaH K I O K'' I' O' /\ CongH O I O' I'). { assert (K <> O) by (intro; subst; Col). apply outH_expand in Hout1; apply outH_expand in Hout2; apply betH_expand in HBet1; apply betH_expand in HBet2; spliter. assert (CongH I' K'' I K) by (apply soustraction_betH with L'' L; try apply between_comm; auto using congH_sym, cong_permr, congH_perml). apply th12; auto using congH_sym, cong_permr, congH_perml; try apply conga_out_conga with O L O' L''; [intro; apply HNC3; ColHR|..]; [intro; apply HNC4; ColHR|..]; try apply outH_trivial; try (right; left); auto. } destruct HT as [HConga6 _]; apply conga_permlr. apply outH_expand in Hout1; apply outH_expand in Hout3; apply outH_expand in Hout4; spliter. apply conga_out_conga with K I K'' I'; try apply outH_trivial; try apply outH_sym; auto; intro; subst; Col. } intros H K O L H' K' O' L' HNC1 HNC2 HNC3 HNC4 HNC5 HNC6 HOS1 HOS2 HConga1 HConga2. destruct (same_side_prime__plane H K O L HOS1) as [p]; spliter. elim (plane_separation K L O H p); trivial; intro HS; [apply th15_aux with L L'; auto| |apply HNC5; Col|apply HNC1; Col]. apply conga_permlr; apply th15_aux with L L'; try solve[intro; Col]; auto; [| |apply OS2__TS; auto]; split; try (intro l ; subst; Col); intros; apply same_side_comm; [destruct HOS1 as [_ HOS1]; apply HOS1; auto|]. destruct HOS2 as [_ HOS2]; apply HOS2; auto. } intros H K O L H' K' O' L' HNC1 HNC2 HNC3 HNC4 HNC5 HNC6 HE HConga1 HConga2. elim HE; clear HE; intros [HTS1 HTS2]; [|apply th15_aux with L L'; auto]. destruct (between_out H O) as [SH HSH]; [intro; subst; Col|]. destruct (between_out H' O') as [SH' HSH']; [intro; subst; Col|]. assert (HConga3 : CongaH SH O L SH' O' L') by (apply conga_permlr; apply th14 with H H'; auto). assert (HConga4 : CongaH SH O K SH' O' K'). { assert (HD1 := betH_distincts _ _ _ HSH); spliter. assert (HD2 := betH_distincts _ _ _ HSH'); spliter. assert (HC1 := between_col _ _ _ HSH). assert (HC2 := between_col _ _ _ HSH'). apply th15_aux with L L'; auto; [intro; apply HNC1; ColHR|intro; apply HNC2; ColHR| intro; apply HNC5; ColHR|intro; apply HNC6; ColHR|..]. { split; [intro; subst; Col|intro l; intros; exists H; split]; [|destruct HTS1 as [_ HTS1]; apply cut_comm; apply HTS1; auto]. split; [intro; apply HNC1; assert (ColH O L SH) by (exists l; auto); ColHR|]. split; [intro; apply HNC1; exists l; auto| exists O; split; try apply between_comm; auto]. } { split; [intro; subst; Col|intro l; intros; exists H'; split]; [|destruct HTS2 as [_ HTS2]; apply cut_comm; apply HTS2; auto]. split; [intro; apply HNC2; assert (ColH O' L' SH') by (exists l; auto); ColHR|]. split; [intro; apply HNC2; exists l; auto| exists O'; split; try apply between_comm; auto]. } } assert (HD1 := betH_distincts _ _ _ HSH); spliter. assert (HD2 := betH_distincts _ _ _ HSH'); spliter. assert (HC1 := between_col _ _ _ HSH). assert (HC2 := between_col _ _ _ HSH'). apply conga_permlr; apply th14 with SH SH'; try apply between_comm; auto; intro; [apply HNC5|apply HNC6]; 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