proposition: Lemma same_side_one_side : forall A B l, same_side A B l -> OS (P1 l) (P2 l) A B.
proof: Proof. unfold same_side. intros. destruct H as [P []]. apply cut_two_sides in H. apply cut_two_sides in H0. eapply l9_8_1. apply H. apply H0. 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