Description: Negation law (even function) for the X sequence. The method of proof used
for the previous four theorems rmxyneg , rmxyadd , rmxy0 , and
rmxy1 via qirropth results in two theorems at once, but typical use
requires only one, so this group of theorems serves to separate the cases.
(Contributed by Stefan O'Rear, 22-Sep-2014)