Ssreflect Users Discussion List

[Georges Gonthier <>]

 by  rewrite val_coset ?rcoset_refl.
You can use val_coset_prim if A is not a group (though the meaning of coset A 
x is somewhat contrived in this case).
-- Georges
-----Original Message-----
From:  [] 
Sent: 16 June 2011 14:57
To: ssreflect
Subject: x \in coset A x

How do I prove that x \in coset A x?  (presumably under the assumption that x 
\in 'N(A))

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone 
Company wrote, ``is the merest claptrap, for there exists no property in 
ideas musical, literary or artistic, except as defined by statute.''