proposition: Lemma same_side_trans : forall A B C l, same_side A B l -> same_side B C l -> same_side A C l.
proof: Proof. intros. apply one_side_same_side. apply same_side_one_side in H. apply same_side_one_side in H0. eapply one_side_transitivity. apply H. assumption. 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