proposition: Lemma cut_two_sides : forall l A B, cut l A B <-> TS (P1 l) (P2 l) A B.
proof: Proof. intros. unfold cut. unfold TS. split. intros. spliter. repeat split; intuition. ex_and H1 T. exists T. unfold IncidentL in H1. unfold Between_H in *. intuition. intros. spliter. ex_and H1 T. unfold IncidentL. repeat split; try assumption. exists T. split. assumption. unfold Between_H. repeat split. assumption. intro. subst. contradiction. intro. subst. contradiction. intro. treat_equalities. 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