proposition: Lemma is_image_perp_in : forall A A' X Y, A <> A' -> X <> Y -> Reflect A A' X Y -> exists P, Perp_at P A A' X Y.
proof: Proof. intros. unfold Reflect in H. induction H1. spliter. unfold ReflectL in H2. spliter. ex_and H2 P. induction H3. exists P. apply perp_in_sym. apply perp_in_right_comm. apply(l8_14_2_1b_bis X Y A' A P); Col. assert_cols. Col. subst A'. tauto. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel