Squares, even and odd elements #
This file proves some general facts about squares, even and odd elements of semirings.
Odd elements are not unified with a multiplicative notion.
Future work #
- TODO: Try to generalize further the typeclass assumptions on
IsSquare/Even. For instance, in some cases, there are
Semiringassumptions that I (DT) am not convinced are necessary.
- TODO: Consider moving the definition and lemmas about
Oddto a separate file.
- TODO: The "old" definition of
Even aasked for the existence of an element
a = 2 * c. For this reason, several fixes introduce an extra
← two_mul. It might be the case that by making a careful choice of
simplemma, this can be avoided.