proposition: Lemma image_preserves_midpoint : forall A B C A' B' C' X Y, ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y -> Midpoint A B C -> Midpoint A' B' C'.
proof: Proof. intros. unfold Midpoint in *. spliter. repeat split. eapply image_preserves_bet. apply H0. apply H. apply H1. apply H2. eapply cong_transitivity. eapply l10_10_spec. apply H0. apply H. eapply cong_transitivity. apply H3. eapply l10_10_spec. apply l10_4_spec. apply H. apply l10_4_spec. apply H1. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity