proposition: Lemma cut_same_side_cut : forall P X Y l, cut l P X -> same_side X Y l -> cut l P Y.
proof: Proof. intros. assert(HC := same_side_not_cut X Y l H0). induction(eq_dec_pointsH X Y). subst Y. assumption. assert(HH0:=H). unfold cut in H. spliter. ex_and H3 A. apply betH_expand in H4. spliter. induction(colH_dec P X Y). unfold cut. repeat split; auto. intro. assert(A <> Y). intro. subst Y. unfold same_side in H0. ex_and H0 M. unfold cut in H11. spliter. contradiction. apply betH_expand in H4. spliter. assert(ColH A X Y). apply (colH_trans P X); Col. col_line H16 m. lines_eq l m. contradiction. exists A. split; auto. apply between_one in H9; auto. induction H9. assert(HH:= betH_trans0 P A X Y H4 H9). intuition. induction H9. assert(A <> Y). intro. subst Y. unfold same_side in H0. ex_and H0 T. unfold cut in H10. spliter. contradiction. assert(BetH P A Y \/ BetH P Y A). apply(betH2_out P A Y X H10 H4); Bet. induction H11. auto. exfalso. apply HC. unfold cut. repeat split; auto. unfold same_side in H0. ex_and H0 T. unfold cut in H12. intuition. exists A. split; auto. assert(HH:= betH_trans0 P Y A X H11 H4). intuition. exfalso. apply HC. unfold cut. repeat split; auto. intro. unfold same_side in H0. ex_and H0 T. unfold cut in H11. intuition. exists A. split; auto. assert(BetH A P Y /\ BetH X A Y). apply(betH_trans0 X A P Y); Bet. intuition. intro. subst Y. apply cut_comm in HH0. contradiction. assert(~IncidL Y l). intro. unfold same_side in H0. ex_and H0 T. unfold cut in H11. spliter. contradiction. destruct (plane_existence P X Y H9) as [p]. spliter. induction (pasch P X Y l p); trivial. contradiction. assert (IncidP A p) by (apply (line_on_plane' P X); Col). destruct (same_side__plane X Y l H0) as [q]; spliter. assert (EqP p q). apply (plane_uniqueness P X Y); trivial. apply (line_on_plane' A X); Col. rewrite H18. assumption. Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms