proposition: Lemma plane_intersection_implies_space_separation : plane_intersection_axiom -> space_separation_axiom.
proof: Proof. intros pint A B C X Y HX HY. assert (HA : Coplanar A B C A) by Cop. destruct (pint A B C A X Y A HA) as [D [HD1 [HD2 HAD]]]; Cop. destruct (cop__one_or_two_sides A D X Y). Cop. intro; apply HX, col_cop2__cop with A D; Col. intro; apply HY, col_cop2__cop with A D; Col. left; apply cop2_ts__tsp with A D; assumption. right; apply cop2_os__osp with A D; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv