proposition: Lemma image_spec_preserves_per : forall A B C A' B' C' X Y, ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y -> Per A B C -> Per A' B' C'.
proof: Proof. intros. induction (eq_dec_points X Y). subst Y. apply image_spec__eq in H. apply image_spec__eq in H0. apply image_spec__eq in H1. subst; assumption. double C B C1. assert (exists C1', ReflectL C1 C1' X Y). apply l10_6_existence_spec. assumption. ex_and H5 C1'. unfold Per. exists C1'. split. eapply image_preserves_midpoint. apply H0. apply H1. apply H6. assumption. eapply cong_transitivity. eapply l10_10_spec. apply H. apply H1. eapply cong_transitivity. unfold Per in H2. ex_and H2 C2. assert (C2=C1). eapply symmetric_point_uniqueness. apply H2. assumption. subst C2. apply H5. eapply l10_10_spec. apply l10_4_spec. apply H. apply l10_4_spec. assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity