proposition: Lemma OS_same_side' : forall P Q A B, OS P Q A B -> same_side' A B P Q.
proof: Proof. intros. unfold same_side'. intros. split. apply OS_distinct with A B;assumption. intros. apply one_side_same_side. destruct l. unfold IncidentL in *. simpl in *. apply col2_os__os with P Q; try assumption; ColR. 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