proposition: Lemma same_side_not_cut : forall A B l, same_side A B l -> ~cut l A B.
proof: Proof. intros. unfold same_side in H. destruct H as [P]. induction(colH_dec P A B). intro. unfold cut in *. spliter. clean_duplicated_hyps. ex_and H8 M. ex_and H6 N. assert(M <> N). intro. subst N. assert(BetH M A B \/ BetH M B A). apply(out2_out P); Bet. intro. destruct H3 as [Q []]. apply betH_expand in H9. intuition. destruct H3 as [R []]. assert(ColH A B M). induction H8; apply between_col in H8; Col. apply betH_expand in H9; spliter. assert(R = M). line A B m H13. col_line H0 mm. lines_eq m mm. col_line H14 nn. lines_eq m nn. col_line H10 pp. lines_eq m pp. apply(inter_incid_uniquenessH P R M l m H7 H17); Col. subst R. induction H8; apply between_only_one' in H9; spliter; contradiction. assert(A <> B). ex_and H3 T. apply betH_distincts in H9. intuition. col_line H0 m. apply H8. apply betH_expand in H2. spliter. col_line H16 mm. lines_eq m mm. apply betH_expand in H6. spliter. col_line H22 nn. lines_eq m nn. apply(inter_incid_uniquenessH P M N l m); auto. destruct H. apply cut_comm in H. apply cut_comm in H1. apply(cut2_not_cut P A B l); auto. 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