proposition: Lemma out_same_side : forall A B C l, IncidL A l -> ~IncidL B l -> outH A B C -> same_side B C l.
proof: Proof. intros. assert(B <> A). apply out_distinct in H1. intuition. assert(HH:= between_out B A H2). destruct HH as [P]. exists P. assert(~IncidL P l). intro. apply betH_expand in H3. spliter. col_line H8 ll. lines_eq l ll. contradiction. split. unfold cut. repeat split; auto. exists A. split; auto. repeat split; auto. intro. unfold outH in H1. induction H1. apply betH_expand in H1. spliter. col_line H9 m. lines_eq l m. contradiction. induction H1. apply betH_expand in H1. spliter. col_line H9 m. lines_eq l m. contradiction. spliter. subst C. contradiction. exists A. split; auto. unfold outH in H1. induction H1. assert(BetH P A C /\ BetH P B C). apply(betH_trans P A B C); Bet. spliter. Bet. induction H1. assert(BetH C A P /\ BetH B C P). apply(betH_trans0 B C A P); Bet. tauto. spliter. subst C. 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