proposition: Lemma pres_bet_line__col : forall {Tm: Tarski_neutral_dimensionless} (f : @Tpoint Tn -> @Tpoint Tm) P Q, P <> Q -> pres_bet_line f P Q -> forall A B C, Col P Q A -> Col P Q B -> Col P Q C -> Col (f A) (f B) (f C).
proof: Proof. intros Tm f P Q HPQ fBet A B C HA HB HC. destruct (col3 P Q A B C) as [HBet|[HBet|HBet]]; trivial; apply fBet in HBet; 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