proposition: Lemma space_separation_implies_plane_intersection : space_separation_axiom -> plane_intersection_axiom.
proof: Proof. intro sep. assert (Haux : forall A B C D E P, Coplanar A B C P -> ~ Col D E P -> exists Q, Coplanar A B C Q /\ Coplanar D E P Q /\ P <> Q). { intros A B C D E P HP1 HP2. destruct (cop_dec A B C D). assert_diffs; exists D; repeat split; Cop. destruct (cop_dec A B C E). assert_diffs; exists E; repeat split; Cop. destruct (sep A B C D E); auto. apply cop_tsp__ex_cop2; assumption. apply cop_osp__ex_cop2; assumption. } intros A B C D E F P HP1 HP2. destruct (ex_ncol_cop2 D E F P) as [D' [E']]. spliter. destruct (Haux A B C D' E' P) as [Q [HQ1 [HQ2 HPQ]]]; Col. exists Q. repeat split; auto. destruct (col_dec D E F) as [HCol|]; [apply col__coplanar, HCol|]. apply coplanar_pseudo_trans with D' E' P; Col; apply coplanar_pseudo_trans with D E F; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv