proposition: Lemma image_in_is_image_spec : forall M A B P P', ReflectL_at M P P' A B -> ReflectL P P' A B.
proof: Proof. intros. unfold ReflectL_at in H. spliter. unfold ReflectL. split. exists M. split; assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop