This file contains results about char_p R 2, in the char_two namespace.
char_p R 2
The lemmas in this file with a _sq suffix are just special cases of the _pow_char lemmas
elsewhere, with a shorter name for ease of discovery, and no need for a [fact (prime 2)] argument.
[fact (prime 2)]