proposition: Lemma congaH_existence_congH : forall A B C O X P U V : Point, U<>V -> ~ ColH P O X -> ~ ColH A B C -> exists Y : Point, CongaH A B C X O Y /\ same_side' P Y O X /\ CongH O Y U V.
proof: Proof. intros. assert (T:=ncolH_distincts A B C H1). assert (T':=ncolH_distincts P O X H0). spliter. elim (cong_4_existence A B C O X P); auto. intros Yaux [HA HB]. assert (O<>Yaux). { apply same_side_prime_not_colH in HB; destruct HB as [_ HFalse]. intro; subst O; apply HFalse; Col. } elim (out_construction O Yaux U V);auto. intros Y [HC HD]. exists Y. split. apply conga_out_conga with A C X Yaux;auto using outH_trivial. split. elim (line_existence O X H3). intros l [HL1 HL2]. assert (same_side Y Yaux l). { apply (out_same_side O Y Yaux);auto. apply (same_side_prime_not_colH P Yaux O X) in HB. spliter. apply outH_expand in HD. intro;apply H10. spliter. assert (ColH O X Y) by (exists l;auto). ColHR. apply outH_sym;auto. apply outH_expand in HD;spliter;auto. } unfold same_side'. split;auto. intros. assert (EqL l0 l). apply line_uniqueness with O X;auto. rewrite H12. unfold same_side' in HB;spliter. specialize H14 with l. apply same_side_trans with Yaux;auto using same_side_comm. assumption. 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