proposition: Remark axiom_hcong_scott: forall P Q A C, A <> C -> P <> Q -> exists B, same_side_scott A B C /\ Cong P Q A B.
proof: Proof. intros. unfold same_side_scott. assert (exists X : Tpoint, Out A X C /\ Cong A X P Q). apply l6_11_existence;auto. decompose [ex and] H1;clear H1. exists x. repeat split. unfold Out in H3. intuition. unfold Out in H3. intuition. apply cols_coincide_2. apply out_col;assumption. unfold Out in H3. unfold Between_H. intro. decompose [and] H3;clear H3. decompose [and] H1;clear H1. clear H8. destruct H7. assert (A = x). eapply between_equality;eauto. intuition. assert (A = C). eapply between_equality;eauto. apply between_symmetry. auto. intuition. Cong. 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