proposition: Lemma extension_reverse_col : forall {Tm: Tarski_neutral_dimensionless} {Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm} (f : @Tpoint Tn -> @Tpoint Tm), extension f -> forall A B C, Col (f A) (f B) (f C) -> Col A B C.
proof: Proof. unfold Col. intros Tm Tm2 f fext A B C HCol. assert (fBetInv := extension_reverse_bet f fext). destruct HCol as [|[|]]; 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