proposition: Lemma axiom_hcong_4_uniqueness : forall A B C O P X Y Y', ~ Col_H P O X -> ~ Col_H A B C -> CongA A B C X O Y -> CongA A B C X O Y' -> same_side' P Y O X -> same_side' P Y' O X -> outH O Y Y'.
proof: Proof. intros. rewrite <- cols_coincide in H. rewrite <- cols_coincide in H0. assert (T:CongA X O Y X O Y'). eapply conga_trans. apply conga_sym. apply H1. assumption. apply out_outH. apply (conga_os__out X). assumption. apply same_side_OS in H3. apply same_side_OS in H4. apply invert_one_side. apply one_side_transitivity with P. apply one_side_symmetry. assumption. 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