proposition: Lemma image_gen_preserves_bet : forall A B C A' B' C' X Y, Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Bet A B C -> Bet A' B' C'.
proof: Proof. intros. destruct (eq_dec_points X Y). subst Y. apply image__midpoint in H. apply image__midpoint in H0. apply image__midpoint in H1. subst. apply l7_15 with A B C X; Midpoint. eapply image_preserves_bet;try apply is_image_is_image_spec; eauto. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity