proposition: Lemma nupper_dim__completeness_for_planes : ~ upper_dim_axiom -> completeness_for_planes.
proof: Proof. intros lowerdim Tm Tm2 M f archi fext A. exfalso; apply lowerdim. apply extension_to_plane__plane with f; trivial. 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