proposition: Lemma ncompleteness_for_3d_spaces__upper_dim_3 : ~ completeness_for_3d_spaces -> upper_dim_3_axiom.
proof: Proof. intro nc. apply upper_dim_3_stab. intro nupper. apply nc, (nupper_dim_3__completeness_for_3d_spaces 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