proposition: Lemma ncompleteness_for_planes__upper_dim : ~ completeness_for_planes -> upper_dim_axiom.
proof: Proof. intro nc. apply upper_dim_stab. intro nupper. apply nc, (nupper_dim__completeness_for_planes nupper). 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