proposition: Lemma same_side__plane : forall A B l, same_side A B l -> exists p, IncidP A p /\ IncidP B p /\ IncidLP l p.
proof: Proof. unfold same_side, cut. intros. destruct H as [P]. spliter. destruct H4 as [X []]. destruct (colH_dec A B P). destruct (other_point_on_line X l H4) as [Y []]. assert (~ ColH X Y A). intro. apply H7. destruct H9 as [m]; spliter. apply inter_incid_uniquenessH with A l m; trivial. destruct (plane_existence X Y A H9) as [p]; spliter. exists p; repeat split. assumption. apply betH_colH in H5; spliter. apply (line_on_plane' A P); Col. apply (line_on_plane' A X); Col. apply (line_on_plane X Y); assumption. destruct (plane_existence A B P H6) as [p]; spliter. exists p. repeat split. assumption. assumption. destruct (ncolH_distincts A B P H6). spliter. destruct H2 as [Y []]. apply (line_on_plane X Y); trivial. intro. subst Y. apply H6. apply betH_colH in H5. spliter. apply colH_trans with X P; Col. apply (line_on_plane' A P); Col. apply (line_on_plane' B P); Col. 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