proposition: Lemma extension__line_extension : forall {Tm: Tarski_neutral_dimensionless} (f : @Tpoint Tn -> @Tpoint Tm) P Q, P <> Q -> extension f -> line_extension f P Q.
proof: Proof. unfold extension, inj, pres_bet, pres_cong, line_extension, inj_line, pres_bet_line, pres_cong_line. intros Tm f P Q HPQ fext; spliter. repeat split; 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