proposition: Lemma image_preserves_per : forall A B C A' B' C' X Y, Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Per A B C -> Per A' B' C'.
proof: Proof. intros. induction (eq_dec_points X Y). - induction H; induction H0; induction H1; spliter; [contradiction..|]. treat_equalities. apply midpoint_preserves_per with A B C X; [|apply l7_2..]; assumption. - induction H; induction H0; induction H1; spliter; [|contradiction..]. apply image_spec_preserves_per with A B C X Y; assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity