proposition: Lemma extension_to_plane__plane : forall {Tm: Tarski_neutral_dimensionless} {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm} {M : Tarski_2D Tm2} (f : @Tpoint Tn -> @Tpoint Tm), extension f -> @upper_dim_axiom Tn.
proof: Proof. intros Tm Tm2 M f fext A B C P Q HPQ H1 H2 H3. apply (extension_reverse_col f); trivial. unfold extension, inj, pres_cong in fext; spliter. unfold Col; apply upper_dim with (f P) (f Q); auto. 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