proposition: Lemma image_in_gen_is_image : forall M A B P P', Reflect_at M P P' A B -> Reflect P P' A B.
proof: Proof. intros. unfold Reflect_at in H. induction H. spliter. apply image_in_is_image_spec in H0. unfold Reflect. tauto. spliter. subst. subst. unfold Reflect. right. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop