proposition: Lemma line_extension_stability : forall {Tm: Tarski_neutral_dimensionless} (f : @Tpoint Tn -> @Tpoint Tm) P Q R, Col P Q R -> P <> R -> line_extension f P Q -> line_extension f P R.
proof: Proof. intros Tm f P Q R HCol HPR [HPQ [fInj [fBet fCong]]]. repeat split; auto; intro; intros; [apply fInj|apply fBet|apply fCong]; trivial; apply col_transitivity_1 with R; Col. 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