I want to use the familiar notation of arithmetic operations on integers in ssreflect (ssrint). I have succeeded (I don't know how to do it better) in using the notation for subtraction by opening distn_scope as follows:
From mathcomp Require Import all_ssreflect ssrint.
Open Scope distn_scope.
Parameter x y : int.
Check x - y : int.
However, I have not been able to use the notation for addition or unary subtraction (minus operation). More specifically, I would like the following Check command to work after the above script.
Check oppzD : - (x + y) = -x + -y.
To solve this problem, what libraries should be loaded (and which scopes should be opened)?
In addition, I would be very happy if you could tell me how to search the manual (or use some commands) to solve this kind of situations.
int uses the generic notations for algebra defined in ring_scope and declared in ssralg.
Regarding finding this kind of things on your own, I only have a hackish solution, hopefully others will know better. You can Check something that uses the objects you want (Check oppzD. in your case is perfect). With oppzD here, you would see things like ssralg.GRing.opp and ssralg.GRing.add, which tells you to look at ssralg. If you had ssralg imported, you would see things like -%R and (_ + _)%R. To look further into it, you can use Set Printing All and Check a notation, e.g. Check (_ + _)%R. This would make GRing.add appear, which you can then Locate. Then, the end of the header documentation of ssralg would tell you about ring_scope.