proposition: Lemma same_side_OS : forall P Q A B, same_side' P Q A B -> OS A B P Q.
proof: Proof. intros. unfold same_side' in *. destruct H. destruct (axiom_line_existence A B H). destruct H1. assert (T:=H0 x H1 H2). assert (U:=same_side_one_side P Q x T). destruct x. unfold IncidentL in *. simpl in *. apply col2_os__os with P1 P2;Col. 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