proposition: Lemma axiom_hcong_4_existence : forall A B C O X P, ~ Col_H P O X -> ~ Col_H A B C -> exists Y, CongA A B C X O Y /\ same_side' P Y O X.
proof: Proof. intros. rewrite <- cols_coincide in H. rewrite <- cols_coincide in H0. assert(~Col X O P). intro. apply H. Col. assert(HH:=angle_construction_1 A B C X O P H0 H1). ex_and HH Y. exists Y. split. assumption. apply OS_same_side'. apply invert_one_side. apply one_side_symmetry. assumption. Qed.
imports: Morphisms GeoCoq.Axioms.hilbert_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Utils.triples