proposition: Lemma line_extension_reverse_bet : forall {Tm: Tarski_neutral_dimensionless} (f : @Tpoint Tn -> @Tpoint Tm) P Q, line_extension f P Q -> forall A B C, Col P Q A -> Col P Q B -> Col P Q C -> Bet (f A) (f B) (f C) -> Bet A B C.
proof: Proof. intros Tm f P Q [HPQ [fInj [fBet fCong]]] A B C HA HB HC HBet. assert (HCol : Col A B C) by (apply (col3 P Q); assumption). destruct HCol as [|[HBet'|HBet']]; trivial; [assert (B = C)|assert (A = B)]; try (subst B; Between); apply fInj; trivial; [apply between_equality with (f A)|apply between_equality with (f C)]; Between. 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