proposition: Lemma line_completeness__completeness_for_planes : line_completeness -> completeness_for_planes.
proof: Proof. intros lc Tm Tm2 M f archi fext A. assert (HB : exists B, Coplanar PA PB PC B /\ f B = A). apply line_completeness_aux; trivial; [exact lower_dim|apply all_coplanar]. destruct HB as [B []]. exists B; assumption. 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