Ssreflect Users Discussion List

[Georges Gonthier <>]

  No, that equation is not really missing: it is covered by a more general 
principal, namely the linearity of composition in its first argument.
Lemmas linearN (as well as raddfN, and even rmorphN if the polynomials are 
over a comRingType) will apply directly, in either direction.
The linearity is documented in the poly.v file header:
            p \Po q == polynomial composition; because this is naturally a  
                      a linear morphism in the first argument, this    
                     notation is transposed (q comes before p for redex 
                    selection, etc).  
 -- Georges

-----Original Message-----
From: bertot [] 
Sent: 05 November 2013 14:12
To: ssreflect
Subject: [ssreflect] Question of style

Hello,

I am using poly.v and I need to reduce

  - 'X \Po p

into -p

It seems that there is a theorem missing, with name comp_poly_opp and 
statement

-p \Po q = -(p \Po q)

or something semantically equivalent.  Do you agree?

Yves