proposition: Lemma one_side_same_side : forall A B l, OS (P1 l) (P2 l) A B -> same_side A B l.
proof: Proof. intros. unfold same_side. unfold OS in H. destruct H as [P []]. exists P. unfold cut. unfold IncidentL. unfold TS in H. unfold TS in H0. spliter. repeat split; auto. ex_and H4 T. exists T. unfold Between_H. repeat split; auto. intro. subst T. contradiction. intro. subst T. contradiction. intro. subst P. apply between_identity in H5. subst T. contradiction. ex_and H2 T. exists T. unfold Between_H. repeat split; auto. intro. subst T. contradiction. intro. subst T. contradiction. intro. subst P. apply between_identity in H5. subst T. contradiction. 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