proposition: Lemma extension_reverse_bet : 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, Bet (f A) (f B) (f C) -> Bet A B C.
proof: Proof. intros Tm Tm2 f [finj [fBet fCong]] A B C HBet. destruct (eq_dec_points (f A) (f B)) as [Heq|]. apply finj in Heq; subst; Between. destruct (segment_construction A B B C) as [D [HD1 HD2]]. assert (C = D); [|subst; auto]. apply finj. apply between_cong_3 with (f A) (f B); Cong. 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