proposition: Lemma line_completeness__completeness_for_3d_spaces : (exists P Q R S, ~ Coplanar P Q R S) -> line_completeness -> completeness_for_3d_spaces.
proof: Proof. intros [P [Q [R [S HNCop]]]] lc Tm Tm2 M f archi fext A. assert (~ Col P Q R) by (apply ncop__ncol with S, HNCop). assert (Haux : forall X, (exists B, Coplanar P Q X B /\ f B = A) -> exists B, f B = A). intros X [B []]; exists B; assumption. destruct (col_dec (f P) (f Q) A). apply (Haux R), line_completeness_aux; Cop. assert (pi : plane_intersection_axiom). { cut upper_dim_3_axiom. apply upper_dim_3_equivalent_axioms; simpl; tauto. unfold upper_dim_3_axiom; exact upper_dim_3. } destruct (pi (f P) (f Q) A (f P) (f R) (f S) (f P)) as [X [HX1 [HX2 HX3]]]; Cop. assert (HY : exists Y, Coplanar P R S Y /\ f Y = X). apply line_completeness_aux; trivial; apply ncop__ncol with Q; Cop. destruct HY as [Y []]; subst. apply (Haux Y), line_completeness_aux; Cop. intro. apply HNCop. apply coplanar_perm_16, col_cop__cop with Y; Col; Cop. intro; subst; apply HX3; reflexivity. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Continuity.grad