proposition: Lemma cong_midpoint__image : forall A B X Y, Cong A X A Y -> Midpoint B X Y -> Reflect Y X A B.
proof: Proof. intros. induction (eq_dec_points A B). right; subst; split; auto. left; repeat split; auto. exists B; split; Col. induction(eq_dec_points X Y). right. assumption. left. apply perp_sym. assert(B <> X /\ B <> Y). apply midpoint_distinct_1. assumption. assumption. spliter. apply col_per_perp; Col. exists Y. split. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop